mathlib documentation

data.set_like

Typeclass for a type A with an injective map to set B #

This typeclass is primarily for use by subobjects like submonoid and submodule.

A typical subobject should be declared as:

structure my_subobject (X : Type*) :=
(carrier : set X)
(op_mem : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)

namespace my_subobject

variables (X : Type*)

instance : set_like (my_subobject X) X :=
⟨sub_mul_action.carrier, λ p q h, by cases p; cases q; congr'⟩

@[simp] lemma mem_carrier {p : my_subobject X} : x ∈ p.carrier ↔ x ∈ (p : set X) := iff.rfl

@[ext] theorem ext {p q : my_subobject X} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h

/-- Copy of a `my_subobject` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (p : my_subobject X) (s : set X) (hs : s = ↑p) : my_subobject X :=
{ carrier := s,
  op_mem' := hs.symm ▸ p.op_mem' }

end my_subobject

This file will then provide a coe_sort, a coe to set, a partial_order, and various extensionality and simp lemmas.

source
@[class]
structure set_like (A : Type u_1) (B : out_param (Type u_2)) :
Type (max u_1 u_2)

A class to indicate that there is a canonical injection between A and set B.

Instances
source
@[protected, instance]
def set_like.set.has_coe_t {A : Type u_1} {B : Type u_2} [i : set_like A B] :
has_coe_t A (set B)
Equations
source
@[protected, instance]
def set_like.has_mem {A : Type u_1} {B : Type u_2} [i : set_like A B] :
has_mem B A
Equations
source
@[protected, nolint, instance]
def set_like.has_coe_to_sort {A : Type u_1} {B : Type u_2} [i : set_like A B] :
has_coe_to_sort A
Equations
source
@[simp, norm_cast]
theorem set_like.coe_sort_coe {A : Type u_1} {B : Type u_2} [i : set_like A B] (p : A) :
↥↑p = ↥p
source
@[protected]
theorem set_like.exists {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} {q : ↥p → Prop} :
(∃ (x : ↥p), q x) ↔ ∃ (x : B) (H : x ∈ p), q ⟨x, H⟩
source
@[protected]
theorem set_like.forall {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} {q : ↥p → Prop} :
(∀ (x : ↥p), q x) ↔ ∀ (x : B) (H : x ∈ p), q ⟨x, H⟩
source
theorem set_like.coe_injective {A : Type u_1} {B : Type u_2} [i : set_like A B] :
function.injective coe
source
@[simp, norm_cast]
theorem set_like.coe_set_eq {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} :
↑p = ↑q ↔ p = q
source
theorem set_like.ext' {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} (h : ↑p = ↑q) :
p = q
source
theorem set_like.ext'_iff {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} :
p = q ↔ ↑p = ↑q
source
theorem set_like.ext {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} (h : ∀ (x : B), x ∈ p ↔ x ∈ q) :
p = q

Note: implementers of set_like must copy this lemma in order to tag it with @[ext].

source
theorem set_like.ext_iff {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} :
p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q
source
@[simp]
theorem set_like.mem_coe {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} {x : B} :
x ∈ ↑p ↔ x ∈ p
source
@[simp, norm_cast]
theorem set_like.coe_eq_coe {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} {x y : ↥p} :
↑x = ↑y ↔ x = y
source
@[simp, norm_cast]
theorem set_like.coe_mk {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} (x : B) (hx : x ∈ p) :
↑⟨x, hx⟩ = x
source
@[simp]
theorem set_like.coe_mem {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} (x : ↥p) :
↑x ∈ p
source
@[protected, simp]
theorem set_like.eta {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} (x : ↥p) (hx : ↑x ∈ p) :
⟨↑x, hx⟩ = x
source
@[protected, nolint, instance]
def set_like.partial_order {A : Type u_1} {B : Type u_2} [i : set_like A B] :
partial_order A
Equations
source
theorem set_like.le_def {A : Type u_1} {B : Type u_2} [i : set_like A B] {S T : A} :
S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T
source
@[simp, norm_cast]
theorem set_like.coe_subset_coe {A : Type u_1} {B : Type u_2} [i : set_like A B] {S T : A} :
↑S ⊆ ↑T ↔ S ≤ T
source
theorem set_like.coe_mono {A : Type u_1} {B : Type u_2} [i : set_like A B] :
monotone coe
source
@[simp, norm_cast]
theorem set_like.coe_ssubset_coe {A : Type u_1} {B : Type u_2} [i : set_like A B] {S T : A} :
↑S ⊂ ↑T ↔ S < T
source
theorem set_like.coe_strict_mono {A : Type u_1} {B : Type u_2} [i : set_like A B] :
strict_mono coe
source
theorem set_like.not_le_iff_exists {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} :
¬p ≤ q ↔ ∃ (x : B) (H : x ∈ p), x ∉ q
source
theorem set_like.exists_of_lt {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} :
p < q → (∃ (x : B) (H : x ∈ q), x ∉ p)
source
theorem set_like.lt_iff_le_and_exists {A : Type u_1} {B : Type u_2} [i : set_like A B] {p q : A} :
p < q ↔ p ≤ q ∧ ∃ (x : B) (H : x ∈ q), x ∉ p