# Documentation

Mathlib.Order.Sublattice

# Sublattices #

This file defines sublattices.

## TODO #

Subsemilattices, if people care about them.

## Tags #

sublattice

structure Sublattice (α : Type u_2) [] :
Type u_2

A sublattice of a lattice is a set containing the suprema and infima of any of its elements.

• carrier : Set α

The underlying set of a sublattice. Do not use directly. Instead, use the coercion Sublattice α → Set α, which Lean should automatically insert for you in most cases.

• supClosed' : SupClosed s.carrier
• infClosed' : InfClosed s.carrier
Instances For
instance Sublattice.instSetLike {α : Type u_2} [] :
SetLike () α
Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]
abbrev Sublattice.ofIsSublattice {α : Type u_2} [] (s : Set α) (hs : ) :

Turn a set closed under supremum and infimum into a sublattice.

Equations
• = { carrier := s, supClosed' := (_ : ), infClosed' := (_ : ) }
Instances For
theorem Sublattice.coe_inj {α : Type u_2} [] {L : } {M : } :
L = M L = M
@[simp]
theorem Sublattice.supClosed {α : Type u_2} [] (L : ) :
@[simp]
theorem Sublattice.infClosed {α : Type u_2} [] (L : ) :
@[simp]
theorem Sublattice.isSublattice {α : Type u_2} [] (L : ) :
@[simp]
theorem Sublattice.mem_carrier {α : Type u_2} [] {L : } {a : α} :
a L.carrier a L
@[simp]
theorem Sublattice.mem_mk {α : Type u_2} [] {s : Set α} {a : α} (h_sup : ) (h_inf : ) :
a { carrier := s, supClosed' := h_sup, infClosed' := h_inf } a s
@[simp]
theorem Sublattice.coe_mk {α : Type u_2} [] {s : Set α} (h_sup : ) (h_inf : ) :
{ carrier := s, supClosed' := h_sup, infClosed' := h_inf } = s
@[simp]
theorem Sublattice.mk_le_mk {α : Type u_2} [] {s : Set α} {t : Set α} (hs_sup : ) (hs_inf : ) (ht_sup : ) (ht_inf : ) :
{ carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } s t
@[simp]
theorem Sublattice.mk_lt_mk {α : Type u_2} [] {s : Set α} {t : Set α} (hs_sup : ) (hs_inf : ) (ht_sup : ) (ht_inf : ) :
{ carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } < { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } s t
def Sublattice.copy {α : Type u_2} [] (L : ) (s : Set α) (hs : s = L) :

Copy of a sublattice with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
• Sublattice.copy L s hs = { carrier := s, supClosed' := (_ : ), infClosed' := (_ : ) }
Instances For
@[simp]
theorem Sublattice.coe_copy {α : Type u_2} [] (L : ) (s : Set α) (hs : s = L) :
(Sublattice.copy L s hs) = s
theorem Sublattice.copy_eq {α : Type u_2} [] (L : ) (s : Set α) (hs : s = L) :
theorem Sublattice.ext {α : Type u_2} [] {L : } {M : } :
(∀ (a : α), a L a M)L = M

Two sublattices are equal if they have the same elements.

instance Sublattice.instSupCoe {α : Type u_2} [] {L : } :
Sup L

A sublattice of a lattice inherits a supremum.

Equations
• Sublattice.instSupCoe = { sup := fun (a b : L) => { val := a b, property := (_ : a b L) } }
instance Sublattice.instInfCoe {α : Type u_2} [] {L : } :
Inf L

A sublattice of a lattice inherits an infimum.

Equations
• Sublattice.instInfCoe = { inf := fun (a b : L) => { val := a b, property := (_ : a b L) } }
@[simp]
theorem Sublattice.coe_sup {α : Type u_2} [] {L : } (a : L) (b : L) :
(a b) = a b
@[simp]
theorem Sublattice.coe_inf {α : Type u_2} [] {L : } (a : L) (b : L) :
(a b) = a b
@[simp]
theorem Sublattice.mk_sup_mk {α : Type u_2} [] {L : } (a : α) (b : α) (ha : a L) (hb : b L) :
{ val := a, property := ha } { val := b, property := hb } = { val := a b, property := (_ : a b L) }
@[simp]
theorem Sublattice.mk_inf_mk {α : Type u_2} [] {L : } (a : α) (b : α) (ha : a L) (hb : b L) :
{ val := a, property := ha } { val := b, property := hb } = { val := a b, property := (_ : a b L) }
instance Sublattice.instLatticeCoe {α : Type u_2} [] (L : ) :
Lattice L

A sublattice of a lattice inherits a lattice structure.

Equations
• One or more equations did not get rendered due to their size.
instance Sublattice.instDistribLatticeCoe {α : Type u_5} [] (L : ) :

A sublattice of a distributive lattice inherits a distributive lattice structure.

Equations
• One or more equations did not get rendered due to their size.
def Sublattice.subtype {α : Type u_2} [] (L : ) :
LatticeHom (L) α

The natural lattice hom from a sublattice to the original lattice.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Sublattice.coe_subtype {α : Type u_2} [] (L : ) :
= Subtype.val
theorem Sublattice.subtype_apply {α : Type u_2} [] (L : ) (a : L) :
a = a
theorem Sublattice.subtype_injective {α : Type u_2} [] (L : ) :
def Sublattice.inclusion {α : Type u_2} [] {L : } {M : } (h : L M) :
LatticeHom L M

The inclusion homomorphism from a sublattice L to a bigger sublattice M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Sublattice.coe_inclusion {α : Type u_2} [] {L : } {M : } (h : L M) :
theorem Sublattice.inclusion_apply {α : Type u_2} [] {L : } {M : } (h : L M) (a : L) :
a =
theorem Sublattice.inclusion_injective {α : Type u_2} [] {L : } {M : } (h : L M) :
@[simp]
theorem Sublattice.inclusion_rfl {α : Type u_2} [] (L : ) :
@[simp]
theorem Sublattice.subtype_comp_inclusion {α : Type u_2} [] {L : } {M : } (h : L M) :
instance Sublattice.instTop {α : Type u_2} [] :
Top ()

The maximum sublattice of a lattice.

Equations
• Sublattice.instTop = { top := { carrier := Set.univ, supClosed' := (_ : SupClosed Set.univ), infClosed' := (_ : InfClosed Set.univ) } }
instance Sublattice.instBot {α : Type u_2} [] :
Bot ()

The empty sublattice of a lattice.

Equations
• Sublattice.instBot = { bot := { carrier := , supClosed' := (_ : ), infClosed' := (_ : ) } }
instance Sublattice.instInf {α : Type u_2} [] :
Inf ()

The inf of two sublattices is their intersection.

Equations
• Sublattice.instInf = { inf := fun (L M : ) => { carrier := L M, supClosed' := (_ : SupClosed (L M)), infClosed' := (_ : InfClosed (L M)) } }
instance Sublattice.instInfSet {α : Type u_2} [] :

The inf of sublattices is their intersection.

Equations
• One or more equations did not get rendered due to their size.
instance Sublattice.instInhabited {α : Type u_2} [] :
Equations
• Sublattice.instInhabited = { default := }
def Sublattice.topEquiv {α : Type u_2} [] :
≃o α

The top sublattice is isomorphic to the lattice.

This is the sublattice version of Equiv.Set.univ α.

Equations
• Sublattice.topEquiv = { toEquiv := , map_rel_iff' := (_ : ∀ {a b : }, () a () b () a () b) }
Instances For
@[simp]
theorem Sublattice.coe_top {α : Type u_2} [] :
= Set.univ
@[simp]
theorem Sublattice.coe_bot {α : Type u_2} [] :
=
@[simp]
theorem Sublattice.coe_inf' {α : Type u_2} [] (L : ) (M : ) :
(L M) = L M
@[simp]
theorem Sublattice.coe_sInf {α : Type u_2} [] (S : Set ()) :
(sInf S) = ⋂ L ∈ S, L
@[simp]
theorem Sublattice.coe_iInf {ι : Sort u_1} {α : Type u_2} [] (f : ι) :
(⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
@[simp]
theorem Sublattice.coe_eq_univ {α : Type u_2} [] {L : } :
L = Set.univ L =
@[simp]
theorem Sublattice.coe_eq_empty {α : Type u_2} [] {L : } :
L = L =
@[simp]
theorem Sublattice.not_mem_bot {α : Type u_2} [] (a : α) :
a
@[simp]
theorem Sublattice.mem_top {α : Type u_2} [] (a : α) :
@[simp]
theorem Sublattice.mem_inf {α : Type u_2} [] {L : } {M : } {a : α} :
a L M a L a M
@[simp]
theorem Sublattice.mem_sInf {α : Type u_2} [] {a : α} {S : Set ()} :
a sInf S LS, a L
@[simp]
theorem Sublattice.mem_iInf {ι : Sort u_1} {α : Type u_2} [] {a : α} {f : ι} :
a ⨅ (i : ι), f i ∀ (i : ι), a f i
instance Sublattice.instCompleteLattice {α : Type u_2} [] :

Sublattices of a lattice form a complete lattice.

Equations
• One or more equations did not get rendered due to their size.
theorem Sublattice.subsingleton_iff {α : Type u_2} [] :
instance Sublattice.instUniqueSublattice {α : Type u_2} [] [] :
Equations
• Sublattice.instUniqueSublattice = { toInhabited := Sublattice.instInhabited, uniq := (_ : ∀ (x : ), x = default) }
def Sublattice.comap {α : Type u_2} {β : Type u_3} [] [] (f : ) (L : ) :

The preimage of a sublattice along a lattice homomorphism.

Equations
Instances For
@[simp]
theorem Sublattice.coe_comap {α : Type u_2} {β : Type u_3} [] [] (L : ) (f : ) :
() = f ⁻¹' L
@[simp]
theorem Sublattice.mem_comap {α : Type u_2} {β : Type u_3} [] [] {f : } {a : α} {L : } :
a f a L
theorem Sublattice.comap_mono {α : Type u_2} {β : Type u_3} [] [] {f : } :
@[simp]
theorem Sublattice.comap_id {α : Type u_2} [] (L : ) :
= L
@[simp]
theorem Sublattice.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (L : ) (g : ) (f : ) :
=
def Sublattice.map {α : Type u_2} {β : Type u_3} [] [] (f : ) (L : ) :

The image of a sublattice along a monoid homomorphism is a sublattice.

Equations
Instances For
@[simp]
theorem Sublattice.coe_map {α : Type u_2} {β : Type u_3} [] [] (f : ) (L : ) :
() = f '' L
@[simp]
theorem Sublattice.mem_map {α : Type u_2} {β : Type u_3} [] [] {L : } {f : } {b : β} :
b ∃ a ∈ L, f a = b
theorem Sublattice.mem_map_of_mem {α : Type u_2} {β : Type u_3} [] [] {L : } (f : ) {a : α} :
a Lf a
theorem Sublattice.apply_coe_mem_map {α : Type u_2} {β : Type u_3} [] [] {L : } (f : ) (a : L) :
f a
theorem Sublattice.map_mono {α : Type u_2} {β : Type u_3} [] [] {f : } :
@[simp]
theorem Sublattice.map_id {α : Type u_2} [] {L : } :
= L
@[simp]
theorem Sublattice.map_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {L : } (g : ) (f : ) :
theorem Sublattice.mem_map_equiv {α : Type u_2} {β : Type u_3} [] [] {L : } {f : α ≃o β} {a : β} :
a Sublattice.map { toSupHom := { toFun := f, map_sup' := (_ : ∀ (a b : α), f (a b) = f a f b) }, map_inf' := (_ : ∀ (a b : α), f (a b) = f a f b) } L () a L
theorem Sublattice.apply_mem_map_iff {α : Type u_2} {β : Type u_3} [] [] {L : } {f : } {a : α} (hf : ) :
f a a L
theorem Sublattice.map_equiv_eq_comap_symm {α : Type u_2} {β : Type u_3} [] [] (f : α ≃o β) (L : ) :
Sublattice.map { toSupHom := { toFun := f, map_sup' := (_ : ∀ (a b : α), f (a b) = f a f b) }, map_inf' := (_ : ∀ (a b : α), f (a b) = f a f b) } L = Sublattice.comap { toSupHom := { toFun := (), map_sup' := (_ : ∀ (a b : β), () (a b) = () a () b) }, map_inf' := (_ : ∀ (a b : β), () (a b) = () a () b) } L
theorem Sublattice.comap_equiv_eq_map_symm {α : Type u_2} {β : Type u_3} [] [] (f : β ≃o α) (L : ) :
Sublattice.comap { toSupHom := { toFun := f, map_sup' := (_ : ∀ (a b : β), f (a b) = f a f b) }, map_inf' := (_ : ∀ (a b : β), f (a b) = f a f b) } L = Sublattice.map { toSupHom := { toFun := (), map_sup' := (_ : ∀ (a b : α), () (a b) = () a () b) }, map_inf' := (_ : ∀ (a b : α), () (a b) = () a () b) } L
theorem Sublattice.map_symm_eq_iff_eq_map {α : Type u_2} {β : Type u_3} [] [] {L : } {M : } {e : β ≃o α} :
Sublattice.map { toSupHom := { toFun := (), map_sup' := (_ : ∀ (a b : α), () (a b) = () a () b) }, map_inf' := (_ : ∀ (a b : α), () (a b) = () a () b) } L = M L = Sublattice.map { toSupHom := { toFun := e, map_sup' := (_ : ∀ (a b : β), e (a b) = e a e b) }, map_inf' := (_ : ∀ (a b : β), e (a b) = e a e b) } M
theorem Sublattice.map_le_iff_le_comap {α : Type u_2} {β : Type u_3} [] [] {L : } {f : } {M : } :
M L
theorem Sublattice.gc_map_comap {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem Sublattice.map_bot {α : Type u_2} {β : Type u_3} [] [] (f : ) :
theorem Sublattice.map_sup {α : Type u_2} {β : Type u_3} [] [] (f : ) (L : ) (M : ) :
theorem Sublattice.map_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] (f : ) (L : ι) :
Sublattice.map f (⨆ (i : ι), L i) = ⨆ (i : ι), Sublattice.map f (L i)
@[simp]
theorem Sublattice.comap_top {α : Type u_2} {β : Type u_3} [] [] (f : ) :
theorem Sublattice.comap_inf {α : Type u_2} {β : Type u_3} [] [] (L : ) (M : ) (f : ) :
theorem Sublattice.comap_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] (f : ) (s : ι) :
Sublattice.comap f (iInf s) = ⨅ (i : ι), Sublattice.comap f (s i)
theorem Sublattice.map_inf_le {α : Type u_2} {β : Type u_3} [] [] (L : ) (M : ) (f : ) :
theorem Sublattice.le_comap_sup {α : Type u_2} {β : Type u_3} [] [] (L : ) (M : ) (f : ) :
theorem Sublattice.le_comap_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] (f : ) (L : ι) :
⨆ (i : ι), Sublattice.comap f (L i) Sublattice.comap f (⨆ (i : ι), L i)
theorem Sublattice.map_inf {α : Type u_2} {β : Type u_3} [] [] (L : ) (M : ) (f : ) (hf : ) :
theorem Sublattice.map_top {α : Type u_2} {β : Type u_3} [] [] (f : ) (h : ) :