doc-next-gen

Mathlib.Data.SetLike.Basic

Module docstring

{"# Typeclass for types with a set-like extensionality property

The Membership typeclass is used to let terms of a type have elements. Many instances of Membership have a set-like extensionality property: things are equal iff they have the same elements. The SetLike typeclass provides a unified interface to define a Membership that is extensional in this way.

The main use of SetLike is for algebraic subobjects (such as Submonoid and Submodule), whose non-proof data consists only of a carrier set. In such a situation, the projection to the carrier set is injective.

In general, a type A is SetLike with elements of type B if it has an injective map to Set B. This module provides standard boilerplate for every SetLike: a coe_sort, a coe to set, a PartialOrder, and various extensionality and simp lemmas.

A typical subobject should be declared as: ``` structure MySubobject (X : Type*) [ObjectTypeclass X] where (carrier : Set X) (op_mem' : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)

namespace MySubobject

variable {X : Type*} [ObjectTypeclass X] {x : X}

instance : SetLike (MySubobject X) X := ⟨MySubobject.carrier, fun p q h => by cases p; cases q; congr!⟩

@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl

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

/-- Copy of a MySubobject with a new carrier equal to the old one. Useful to fix definitional equalities. See Note [range copy pattern]. -/ protected def copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) : MySubobject X := { carrier := s opmem' := hs.symm ▸ p.opmem' }

@[simp] lemma coe_copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) : (p.copy s hs : Set X) = s := rfl

lemma copyeq (p : MySubobject X) (s : Set X) (hs : s = ↑p) : p.copy s hs = p := SetLike.coeinjective hs

end MySubobject ```

An alternative to SetLike could have been an extensional Membership typeclass: class ExtMembership (α : out_param <| Type u) (β : Type v) extends Membership α β where (ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t) While this is equivalent, SetLike conveniently uses a carrier set projection directly.

Tags

subobjects "}

SetLike structure
(A : Type*) (B : outParam Type*)
Full source 
/-- A class to indicate that there is a canonical injection between `A` and `Set B`.

This has the effect of giving terms of `A` elements of type `B` (through a `Membership`
instance) and a compatible coercion to `Type*` as a subtype.

Note: if `SetLike.coe` is a projection, implementers should create a simp lemma such as
```
@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
```
to normalize terms.

If you declare an unbundled subclass of `SetLike`, for example:
```
class MulMemClass (S : Type*) (M : Type*) [Mul M] [SetLike S M] where
  ...
```
Then you should *not* repeat the `outParam` declaration so `SetLike` will supply the value instead.
This ensures your subclass will not have issues with synthesis of the `[Mul M]` parameter starting
before the value of `M` is known.
-/
@[notation_class * carrier Simps.findCoercionArgs]
class SetLike (A : Type*) (B : outParam Type*) where
  /-- The coercion from a term of a `SetLike` to its corresponding `Set`. -/
  protected coe : A → Set B
  /-- The coercion from a term of a `SetLike` to its corresponding `Set` is injective. -/
  protected coe_injective' : Function.Injective coe
Set-like Structure with Extensionality
Informal description
The `SetLike` structure provides a way to associate a type `A` with a set of elements of type `B` via an injective coercion. This allows terms of type `A` to be treated as sets of elements of type `B`, with a membership relation and a coercion to the type of subsets of `B`. Specifically, for a type `A` to be `SetLike` with elements of type `B`, there must be an injective function from `A` to `Set B`. This setup enables extensionality: two terms of `A` are equal if and only if they contain the same elements of type `B`. This structure is particularly useful for algebraic subobjects (such as subgroups, submodules, etc.), where the non-proof data consists solely of a carrier set, and the coercion to the carrier set is injective.
SetLike.instCoeTCSet instance
: CoeTC A (Set B)
Full source 
instance : CoeTC A (Set B) where coe := SetLike.coe
Coercion from Set-like Structures to Subsets
Informal description
For any set-like structure $A$ with elements of type $B$, there is a canonical coercion from $A$ to the type of subsets of $B$. This means that any element of $A$ can be treated as a subset of $B$ via an injective function.
SetLike.instMembership instance
: Membership B A
Full source 
instance (priority := 100) instMembership : Membership B A :=
  ⟨fun p x => x ∈ (p : Set B)⟩
Membership Relation for Set-like Structures
Informal description
For any set-like structure $A$ with elements of type $B$, there is a canonical membership relation $\in$ between elements of $B$ and elements of $A$. This means that for any $x : B$ and $S : A$, we can write $x \in S$ to indicate that $x$ is a member of the set-like structure $S$.
SetLike.instCoeSortType instance
: CoeSort A (Type _)
Full source 
instance (priority := 100) : CoeSort A (Type _) :=
  ⟨fun p => { x : B // x ∈ p }⟩
Coercion from Set-like Structures to Types
Informal description
For any set-like structure $A$ with elements of type $B$, there is a canonical coercion from $A$ to the type of subsets of $B$. This means that any element of $A$ can be treated as a type whose elements are the members of the corresponding subset of $B$.
SetLike.delabSubtypeSetLike definition
: Delab
Full source 
/-- For terms that match the `CoeSort` instance's body, pretty print as `↥S`
rather than as `{ x // x ∈ S }`. The discriminating feature is that membership
uses the `SetLike.instMembership` instance. -/
@[app_delab Subtype]
def delabSubtypeSetLike : Delab := whenPPOption getPPNotation do
  let #[_, .lam n _ body _] := (← getExpr).getAppArgs | failure
  guardguard <| body.isAppOf ``Membership.mem
  let #[_, _, inst, _, .bvar 0] := body.getAppArgs | failure
  guardguard <| inst.isAppOfArity ``instMembership 3
  let S ← withAppArg <| withBindingBody n <| withNaryArg 3 delab
  `(↥$S)
Pretty printing for `SetLike` subtypes
Informal description
A pretty printing rule that displays terms of a subtype `{x // x ∈ S}` as `↥S` when the membership is defined via the `SetLike` typeclass. This rule ensures that terms matching the `CoeSort` instance are displayed in a more readable form.
SetLike.coe_sort_coe theorem
: ((p : Set B) : Type _) = p
Full source 
@[simp, norm_cast]
theorem coe_sort_coe : ((p : Set B) : Type _) = p :=
  rfl
Identity Coercion from Set to Type
Informal description
For any set $p$ of elements of type $B$, the type obtained by coercing $p$ to a sort (via `CoeSort`) is equal to $p$ itself. In other words, the coercion from `Set B` to `Type _` is the identity function.
SetLike.exists theorem
{q : p → Prop} : (∃ x, q x) ↔ ∃ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩
Full source 
protected theorem «exists» {q : p → Prop} : (∃ x, q x) ↔ ∃ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩ :=
  SetCoe.exists
Existence in Set-like Structure vs Existence in Base Type
Informal description
For any set-like structure $p$ with elements of type $B$ and any predicate $q$ on elements of $p$, there exists an element $x$ in $p$ satisfying $q(x)$ if and only if there exists an element $x$ of type $B$ with $x \in p$ such that $q(\langle x, h\rangle)$ holds (where $h$ is the proof that $x \in p$).
SetLike.forall theorem
{q : p → Prop} : (∀ x, q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩
Full source 
protected theorem «forall» {q : p → Prop} : (∀ x, q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩ :=
  SetCoe.forall
Universal Quantification over Set-like Structures
Informal description
For any set-like structure $p$ with elements of type $B$ and any predicate $q$ on elements of $p$, the following are equivalent: 1. For every element $x$ in $p$, $q(x)$ holds. 2. For every element $x$ of type $B$ with $x \in p$, $q(\langle x, h\rangle)$ holds (where $h$ is the proof that $x \in p$).
SetLike.coe_injective theorem
: Function.Injective (SetLike.coe : A → Set B)
Full source 
theorem coe_injective : Function.Injective (SetLike.coe : A → Set B) := fun _ _ h =>
  SetLike.coe_injective' h
Injectivity of Set-Like Coercion
Informal description
For any set-like structure `A` with elements of type `B`, the coercion function from `A` to `Set B` is injective. That is, if two elements of `A` have the same carrier set, then they are equal.
SetLike.coe_set_eq theorem
: (p : Set B) = q ↔ p = q
Full source 
@[simp, norm_cast]
theorem coe_set_eq : (p : Set B) = q ↔ p = q :=
  coe_injective.eq_iff
Equality of Set-Like Elements via Coercion to Sets
Informal description
For any two elements $p$ and $q$ of a set-like structure $A$ with elements of type $B$, the coercion of $p$ to a set equals the coercion of $q$ to a set if and only if $p$ and $q$ are equal as elements of $A$. In other words, $(p : \text{Set } B) = q \leftrightarrow p = q$.
SetLike.coe_ne_coe theorem
: (p : Set B) ≠ q ↔ p ≠ q
Full source 
@[norm_cast] lemma coe_ne_coe : (p : Set B) ≠ q(p : Set B) ≠ q ↔ p ≠ q := coe_injective.ne_iff
Inequality of Set-Like Elements via Coercion to Sets
Informal description
For any two elements $p$ and $q$ of a set-like structure $A$ with elements of type $B$, the coercion of $p$ to a set is not equal to the coercion of $q$ to a set if and only if $p$ and $q$ are not equal as elements of $A$. In other words, $(p : \text{Set } B) \neq q \leftrightarrow p \neq q$.
SetLike.ext' theorem
(h : (p : Set B) = q) : p = q
Full source 
theorem ext' (h : (p : Set B) = q) : p = q :=
  coe_injective h
Equality of Set-Like Elements via Carrier Set Equality
Informal description
For any two elements $p$ and $q$ of a set-like structure $A$ with elements of type $B$, if their carrier sets (as subsets of $B$) are equal, then $p$ and $q$ are equal.
SetLike.ext'_iff theorem
: p = q ↔ (p : Set B) = q
Full source 
theorem ext'_iff : p = q ↔ (p : Set B) = q :=
  coe_set_eq.symm
Equality of Set-Like Elements via Carrier Set Equality
Informal description
For any two elements $p$ and $q$ of a set-like structure $A$ with elements of type $B$, they are equal if and only if their coercions to sets (i.e., their carrier sets) are equal. In other words, $p = q \leftrightarrow (p : \text{Set } B) = q$.
SetLike.ext theorem
(h : ∀ x, x ∈ p ↔ x ∈ q) : p = q
Full source 
/-- Note: implementers of `SetLike` must copy this lemma in order to tag it with `@[ext]`. -/
theorem ext (h : ∀ x, x ∈ px ∈ p ↔ x ∈ q) : p = q :=
  coe_injective <| Set.ext h
Extensionality of Set-like Structures: $p = q \iff \forall x, x \in p \leftrightarrow x \in q$
Informal description
For any two elements $p$ and $q$ of a set-like structure $A$ with elements of type $B$, if for every $x \in B$ we have $x \in p$ if and only if $x \in q$, then $p = q$.
SetLike.ext_iff theorem
: p = q ↔ ∀ x, x ∈ p ↔ x ∈ q
Full source 
theorem ext_iff : p = q ↔ ∀ x, x ∈ p ↔ x ∈ q :=
  coe_injective.eq_iff.symm.trans Set.ext_iff
Extensionality Criterion for Set-like Structures: $p = q \iff \forall x, x \in p \leftrightarrow x \in q$
Informal description
For any two elements $p$ and $q$ of a set-like structure $A$ with elements of type $B$, the equality $p = q$ holds if and only if for every element $x$ of type $B$, the membership $x \in p$ is equivalent to $x \in q$.
SetLike.mem_coe theorem
{x : B} : x ∈ (p : Set B) ↔ x ∈ p
Full source 
@[simp]
theorem mem_coe {x : B} : x ∈ (p : Set B)x ∈ (p : Set B) ↔ x ∈ p :=
  Iff.rfl
Membership Equivalence in Set-like Structures: $x \in (p : \mathrm{Set}\, B) \leftrightarrow x \in p$
Informal description
For any element $x$ of type $B$ and any set-like structure $p$ (with elements of type $B$), the statement $x$ belongs to the coercion of $p$ to $\mathrm{Set}\, B$ is equivalent to $x$ belonging to $p$ itself. In other words, $x \in (p : \mathrm{Set}\, B) \leftrightarrow x \in p$.
SetLike.coe_eq_coe theorem
{x y : p} : (x : B) = y ↔ x = y
Full source 
@[simp, norm_cast]
theorem coe_eq_coe {x y : p} : (x : B) = y ↔ x = y :=
  Subtype.ext_iff_val.symm
Equality of Coerced Elements in Set-like Structures
Informal description
For any two elements $x$ and $y$ of a set-like structure $p$ (of type $A$ with elements of type $B$), the equality of their coerced values in $B$ is equivalent to their equality in $p$. That is, $(x : B) = y \leftrightarrow x = y$.
SetLike.coe_mem theorem
(x : p) : (x : B) ∈ p
Full source 
@[simp]
theorem coe_mem (x : p) : (x : B) ∈ p :=
  x.2
Membership of Coerced Element in Set-like Structure
Informal description
For any element $x$ of a set-like structure $p$ (with elements of type $B$), the coerced value of $x$ in $B$ is a member of $p$. In other words, if $x \in p$ as an element of the structure, then $x \in p$ when viewed as an element of $B$.
SetLike.mem_of_subset theorem
{s : Set B} (hp : s ⊆ p) {x : B} (hx : x ∈ s) : x ∈ p
Full source 
@[aesop 5% apply (rule_sets := [SetLike])]
lemma mem_of_subset {s : Set B} (hp : s ⊆ p) {x : B} (hx : x ∈ s) : x ∈ p := hp hx
Membership Preservation under Subset Inclusion in Set-like Structures
Informal description
For any subset $s$ of a set-like structure $p$ (with elements of type $B$), if $s \subseteq p$ and $x \in s$ for some $x : B$, then $x \in p$.
SetLike.eta theorem
(x : p) (hx : (x : B) ∈ p) : (⟨x, hx⟩ : p) = x
Full source 
@[simp]
protected theorem eta (x : p) (hx : (x : B) ∈ p) : (⟨x, hx⟩ : p) = x := rfl
Eta Reduction for Set-like Structures
Informal description
For any element $x$ of a set-like structure $p$ (with elements of type $B$), if $x$ is a member of $p$ (i.e., $x \in p$), then the pair $\langle x, hx \rangle$ (where $hx$ is the proof that $x \in p$) is equal to $x$ itself when viewed as an element of $p$.
SetLike.setOf_mem_eq theorem
(a : A) : {b | b ∈ a} = a
Full source 
@[simp] lemma setOf_mem_eq (a : A) : {b | b ∈ a} = a := rfl
Set Comprehension Equals Original Set in Set-like Structures
Informal description
For any element $a$ of a set-like structure $A$ with elements of type $B$, the set $\{b \mid b \in a\}$ is equal to $a$ itself.
SetLike.instPartialOrder instance
: PartialOrder A
Full source 
instance (priority := 100) instPartialOrder : PartialOrder A :=
  { PartialOrder.lift (SetLike.coe : A → Set B) coe_injective with
    le := fun H K => ∀ ⦃x⦄, x ∈ H → x ∈ K }
Partial Order on Set-like Structures
Informal description
For any set-like structure $A$ with elements of type $B$, there is a canonical partial order on $A$ where $S \leq T$ if and only if every element of $S$ is also an element of $T$.
SetLike.le_def theorem
{S T : A} : S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T
Full source 
theorem le_def {S T : A} : S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T :=
  Iff.rfl
Partial Order Definition for Set-like Structures: $S \leq T \leftrightarrow \forall x \in B, x \in S \to x \in T$
Informal description
For any two elements $S$ and $T$ of a set-like structure $A$ with elements of type $B$, the inequality $S \leq T$ holds if and only if every element $x \in B$ that belongs to $S$ also belongs to $T$.
SetLike.coe_subset_coe theorem
{S T : A} : (S : Set B) ⊆ T ↔ S ≤ T
Full source 
@[simp, norm_cast] lemma coe_subset_coe {S T : A} : (S : Set B) ⊆ T(S : Set B) ⊆ T ↔ S ≤ T := .rfl
Subset Relation on Coerced Set-like Structures
Informal description
For any two set-like structures $S$ and $T$ of type $A$ with elements of type $B$, the subset relation $(S : \text{Set } B) \subseteq T$ holds if and only if $S$ is less than or equal to $T$ in the partial order on $A$.
SetLike.coe_ssubset_coe theorem
{S T : A} : (S : Set B) ⊂ T ↔ S < T
Full source 
@[simp, norm_cast] lemma coe_ssubset_coe {S T : A} : (S : Set B) ⊂ T(S : Set B) ⊂ T ↔ S < T := .rfl
Strict Subset Correspondence for Set-like Structures
Informal description
For any two set-like structures $S$ and $T$ of type $A$ with elements of type $B$, the coercion of $S$ to a set is a strict subset of the coercion of $T$ to a set if and only if $S$ is strictly less than $T$ in the partial order on $A$.
SetLike.coe_mono theorem
: Monotone (SetLike.coe : A → Set B)
Full source 
@[mono]
theorem coe_mono : Monotone (SetLike.coe : A → Set B) := fun _ _ => coe_subset_coe.mpr
Monotonicity of Set-like Coercion
Informal description
The coercion function from a set-like structure $A$ to the type of sets over $B$ is monotone with respect to the partial order on $A$ and the subset relation on $\text{Set } B$. That is, for any $S, T \in A$, if $S \leq T$ then $(S : \text{Set } B) \subseteq (T : \text{Set } B)$.
SetLike.coe_strictMono theorem
: StrictMono (SetLike.coe : A → Set B)
Full source 
@[mono]
theorem coe_strictMono : StrictMono (SetLike.coe : A → Set B) := fun _ _ => coe_ssubset_coe.mpr
Strict Monotonicity of Coercion from Set-like Structures to Sets
Informal description
The coercion function from a set-like structure $A$ to the type of sets over $B$ is strictly monotone. That is, for any $S, T \in A$, if $S < T$ in the partial order on $A$, then the set corresponding to $S$ is a strict subset of the set corresponding to $T$.
SetLike.not_le_iff_exists theorem
: ¬p ≤ q ↔ ∃ x ∈ p, x ∉ q
Full source 
theorem not_le_iff_exists : ¬p ≤ q¬p ≤ q ↔ ∃ x ∈ p, x ∉ q :=
  Set.not_subset
Characterization of Non-Inclusion in Set-like Structures
Informal description
For any two set-like structures $p$ and $q$ of type $A$ with elements of type $B$, the statement that $p$ is not less than or equal to $q$ is equivalent to the existence of an element $x \in p$ such that $x \notin q$. In other words, $\neg (p \leq q) \leftrightarrow \exists x \in p, x \notin q$.
SetLike.exists_of_lt theorem
: p < q → ∃ x ∈ q, x ∉ p
Full source 
theorem exists_of_lt : p < q → ∃ x ∈ q, x ∉ p :=
  Set.exists_of_ssubset
Existence of Element in Strictly Larger Set-like Structure
Informal description
For any two set-like structures $p$ and $q$ of type $A$ with elements of type $B$, if $p$ is strictly less than $q$ in the partial order on $A$, then there exists an element $x \in q$ such that $x \notin p$.
SetLike.lt_iff_le_and_exists theorem
: p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p
Full source 
theorem lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p := by
  rw [lt_iff_le_not_le, not_le_iff_exists]
Characterization of Strict Inclusion in Set-like Structures: $p < q \leftrightarrow (p \subseteq q) \land (\exists x \in q, x \notin p)$
Informal description
For any two set-like structures $p$ and $q$ of type $A$ with elements of type $B$, the strict inequality $p < q$ holds if and only if $p$ is contained in $q$ (i.e., $p \leq q$) and there exists an element $x \in q$ that is not in $p$.
SetLike.instSubtypeSet abbrev
{X} {p : Set X → Prop} : SetLike { s // p s } X
Full source 
/-- membership is inherited from `Set X` -/
abbrev instSubtypeSet {X} {p : Set X → Prop} : SetLike {s // p s} X where
  coe := (↑)
  coe_injective' := Subtype.val_injective
Subtype of Power Set as Set-Like Structure
Informal description
For any type $X$ and a predicate $p$ on the power set of $X$, the subtype $\{s \mid p(s)\}$ of $\mathcal{P}(X)$ (the set of all subsets of $X$ satisfying $p$) is a `SetLike` structure with elements of type $X$. This means that elements of this subtype can be treated as sets of elements of $X$ with an injective coercion to $\mathcal{P}(X)$.
SetLike.instSubtype abbrev
{X S} [SetLike S X] {p : S → Prop} : SetLike { s // p s } X
Full source 
/-- membership is inherited from `S` -/
abbrev instSubtype {X S} [SetLike S X] {p : S → Prop} : SetLike {s // p s} X where
  coe := (↑)
  coe_injective' := SetLike.coe_injective.comp Subtype.val_injective
Subtype of Set-like Structure is Set-like
Informal description
Given a type $X$ and a `SetLike` structure $S$ on $X$, for any predicate $p$ on $S$, the subtype $\{s : S \mid p(s)\}$ inherits a `SetLike` structure with elements of type $X$. This means that elements of this subtype can be treated as sets of elements of $X$ with an injective coercion to $\mathcal{P}(X)$.
SetLike.mem_mk_set theorem
{X} {p : Set X → Prop} {U : Set X} {h : p U} {x : X} : x ∈ Subtype.mk U h ↔ x ∈ U
Full source 
@[simp] lemma mem_mk_set {X} {p : Set X → Prop} {U : Set X} {h : p U} {x : X} :
    x ∈ Subtype.mk U hx ∈ Subtype.mk U h ↔ x ∈ U := Iff.rfl
Membership in Subtype of Power Set
Informal description
For any type $X$, predicate $p$ on sets of $X$, set $U \subseteq X$ satisfying $p$, and element $x \in X$, we have $x \in \langle U, h\rangle$ if and only if $x \in U$, where $\langle U, h\rangle$ denotes the subtype element constructed from $U$ with proof $h$ that $p(U)$ holds.
SetLike.mem_mk theorem
{X S} [SetLike S X] {p : S → Prop} {U : S} {h : p U} {x : X} : x ∈ Subtype.mk U h ↔ x ∈ U
Full source 
@[simp] lemma mem_mk {X S} [SetLike S X] {p : S → Prop} {U : S} {h : p U} {x : X} :
    x ∈ Subtype.mk U hx ∈ Subtype.mk U h ↔ x ∈ U := Iff.rfl
Membership in Subtype of Set-like Structure
Informal description
For any type $X$ and any set-like structure $S$ on $X$ (i.e., $S$ is an instance of `SetLike` with elements of type $X$), given a predicate $p$ on $S$, an element $U \in S$ satisfying $p$, and an element $x \in X$, we have $x \in \langle U, h\rangle$ if and only if $x \in U$, where $\langle U, h\rangle$ denotes the subtype element constructed from $U$ with proof $h$ that $p(U)$ holds.