mathlib3 documentation

data.set_like.basic

Typeclass for types with a set-like extensionality property #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

The main use of set_like 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 set_like with elements of type B if it has an injective map to set B. This module provides standard boilerplate for every set_like: a coe_sort, a coe to set, a partial_order, and various extensionality and simp lemmas.

A typical subobject should be declared as:

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

namespace my_subobject

variables {X : Type*} [object_typeclass X] {x : X}

instance : set_like (my_subobject X) X :=
⟨my_subobject.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. See Note [range copy pattern]. -/
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' }

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

lemma copy_eq (p : my_subobject X) (s : set X) (hs : s = ↑p) : p.copy s hs = p :=
set_like.coe_injective hs

end my_subobject

An alternative to set_like could have been an extensional has_mem typeclass:

class has_ext_mem (α : out_param $ Type u) (β : Type v) extends has_mem α β :=
(ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)

While this is equivalent, set_like conveniently uses a carrier set projection directly.

Tags #

subobjects

@[class]

structure set_like (A : Type u_1) (B : out_param (Type u_2)) :

Type (max u_1 u_2)

coe : A → set B
coe_injective' : function.injective set_like.coe

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 has_mem instance) and a compatible coercion to Type* as a subtype.

Note: if set_like.coe is a projection, implementers should create a simp lemma such as

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

to normalize terms.

If you declare an unbundled subclass of set_like, for example:

class mul_mem_class (S : Type*) (M : Type*) [has_mul M] [set_like S M] where
  ...

Then you should not repeat the out_param declaration, set_like will supply the value instead. This ensures in Lean 4 your subclass will not have issues with synthesis of the [has_mul M] parameter starting before the value of M is known.

Instances of this typeclass

Instances of other typeclasses for set_like

set_like.has_sizeof_inst

@[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

set_like.set.has_coe_t = {coe := set_like.coe i}

@[protected, instance]

def set_like.has_mem {A : Type u_1} {B : Type u_2} [i : set_like A B] :

Equations

set_like.has_mem = {mem := λ (x : B) (p : A), x ∈ ↑p}

@[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 (Type u_2)

Equations

set_like.has_coe_to_sort = {coe := λ (p : A), {x // x ∈ p}}

@[simp, norm_cast]

theorem set_like.coe_sort_coe {A : Type u_1} {B : Type u_2} [i : set_like A B] (p : A) :

@[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⟩

@[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⟩

theorem set_like.coe_injective {A : Type u_1} {B : Type u_2} [i : set_like A B] :

function.injective coe

@[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

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

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

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].

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

@[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

@[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

@[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

@[simp]

theorem set_like.coe_mem {A : Type u_1} {B : Type u_2} [i : set_like A B] {p : A} (x : ↥p) :

@[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

@[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

set_like.partial_order = {le := λ (H K : A), ∀ ⦃x : B⦄, x ∈ H → x ∈ K, lt := partial_order.lt (partial_order.lift coe set_like.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

@[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

theorem set_like.coe_mono {A : Type u_1} {B : Type u_2} [i : set_like A B] :

@[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

theorem set_like.coe_strict_mono {A : Type u_1} {B : Type u_2} [i : set_like A B] :

strict_mono coe

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

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)

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