Sublattices

This file defines sublattices.

TODO

Subsemilattices, if people care about them.

Tags

sublattice

structure Sublattice (α : Type u_2) [Lattice α] : 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 self.carrier
• infClosed' : InfClosed self.carrier

@[implicit_reducible]

instance Sublattice.instSetLike {α : Type u_2} [Lattice α] : SetLike (Sublattice α) α

Equations

• Sublattice.instSetLike = { coe := fun (L : Sublattice α) => L.carrier, coe_injective' := ⋯ }

@[implicit_reducible]

instance Sublattice.instPartialOrder {α : Type u_2} [Lattice α] : PartialOrder (Sublattice α)

Equations

• Sublattice.instPartialOrder = PartialOrder.ofSetLike (Sublattice α) α

def Sublattice.Simps.coe {α : Type u_2} [Lattice α] (L : Sublattice α) : Set α

See Note [custom simps projection].

Equations

• Sublattice.Simps.coe L = ↑L

@[reducible, inline]

abbrev Sublattice.ofIsSublattice {α : Type u_2} [Lattice α] (s : Set α) (hs : IsSublattice s) : Sublattice α

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

Equations

• Sublattice.ofIsSublattice s hs = { carrier := s, supClosed' := ⋯, infClosed' := ⋯ }

theorem Sublattice.coe_inj {α : Type u_2} [Lattice α] {L M : Sublattice α} : ↑L = ↑M ↔ L = M

@[simp]

theorem Sublattice.supClosed {α : Type u_2} [Lattice α] (L : Sublattice α) : SupClosed ↑L

@[simp]

theorem Sublattice.infClosed {α : Type u_2} [Lattice α] (L : Sublattice α) : InfClosed ↑L

theorem Sublattice.sup_mem {α : Type u_2} [Lattice α] {L : Sublattice α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a ⊔ b ∈ L

theorem Sublattice.inf_mem {α : Type u_2} [Lattice α] {L : Sublattice α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a ⊓ b ∈ L

@[simp]

theorem Sublattice.isSublattice {α : Type u_2} [Lattice α] (L : Sublattice α) : IsSublattice ↑L

@[simp]

theorem Sublattice.mem_carrier {α : Type u_2} [Lattice α] {L : Sublattice α} {a : α} : a ∈ L.carrier ↔ a ∈ L

@[simp]

theorem Sublattice.mem_mk {α : Type u_2} [Lattice α] {s : Set α} {a : α} (h_sup : SupClosed s) (h_inf : InfClosed s) : a ∈ { carrier := s, supClosed' := h_sup, infClosed' := h_inf } ↔ a ∈ s

@[simp]

theorem Sublattice.coe_mk {α : Type u_2} [Lattice α] {s : Set α} (h_sup : SupClosed s) (h_inf : InfClosed s) : ↑{ carrier := s, supClosed' := h_sup, infClosed' := h_inf } = s

@[simp]

theorem Sublattice.mk_le_mk {α : Type u_2} [Lattice α] {s t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t) (ht_inf : InfClosed t) : { 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} [Lattice α] {s t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t) (ht_inf : InfClosed t) : { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } < { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔ s ⊂ t

def Sublattice.copy {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L) : Sublattice α

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

Equations

• L.copy s hs = { carrier := s, supClosed' := ⋯, infClosed' := ⋯ }

@[simp]

theorem Sublattice.coe_copy {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L) : ↑(L.copy s hs) = s

theorem Sublattice.copy_eq {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L) : L.copy s hs = L

theorem Sublattice.ext {α : Type u_2} [Lattice α] {L M : Sublattice α} : (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M

Two sublattices are equal if they have the same elements.

@[implicit_reducible]

instance Sublattice.instSupCoe {α : Type u_2} [Lattice α] {L : Sublattice α} : Max ↥L

A sublattice of a lattice inherits a supremum.

Equations

• Sublattice.instSupCoe = { max := fun (a b : ↥L) => ⟨↑a ⊔ ↑b, ⋯⟩ }

@[implicit_reducible]

instance Sublattice.instInfCoe {α : Type u_2} [Lattice α] {L : Sublattice α} : Min ↥L

A sublattice of a lattice inherits an infimum.

Equations

• Sublattice.instInfCoe = { min := fun (a b : ↥L) => ⟨↑a ⊓ ↑b, ⋯⟩ }

@[simp]

theorem Sublattice.coe_sup {α : Type u_2} [Lattice α] {L : Sublattice α} (a b : ↥L) : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem Sublattice.coe_inf {α : Type u_2} [Lattice α] {L : Sublattice α} (a b : ↥L) : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem Sublattice.mk_sup_mk {α : Type u_2} [Lattice α] {L : Sublattice α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩

@[simp]

theorem Sublattice.mk_inf_mk {α : Type u_2} [Lattice α] {L : Sublattice α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩

@[implicit_reducible]

instance Sublattice.instLatticeCoe {α : Type u_2} [Lattice α] (L : Sublattice α) : Lattice ↥L

A sublattice of a lattice inherits a lattice structure.

Equations

• L.instLatticeCoe = Function.Injective.lattice (fun (a : ↥L) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance Sublattice.instDistribLatticeCoe {α : Type u_5} [DistribLattice α] (L : Sublattice α) : DistribLattice ↥L

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

Equations

• L.instDistribLatticeCoe = Function.Injective.distribLattice (fun (a : ↥L) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯

def Sublattice.subtype {α : Type u_2} [Lattice α] (L : Sublattice α) : LatticeHom (↥L) α

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

Equations

• L.subtype = { toFun := Subtype.val, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem Sublattice.coe_subtype {α : Type u_2} [Lattice α] (L : Sublattice α) : ⇑L.subtype = Subtype.val

theorem Sublattice.subtype_apply {α : Type u_2} [Lattice α] (L : Sublattice α) (a : ↥L) : L.subtype a = ↑a

theorem Sublattice.subtype_injective {α : Type u_2} [Lattice α] (L : Sublattice α) : Function.Injective ⇑L.subtype

def Sublattice.inclusion {α : Type u_2} [Lattice α] {L M : Sublattice α} (h : L ≤ M) : LatticeHom ↥L ↥M

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

Equations

• Sublattice.inclusion h = { toFun := Set.inclusion h, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem Sublattice.coe_inclusion {α : Type u_2} [Lattice α] {L M : Sublattice α} (h : L ≤ M) : ⇑(inclusion h) = Set.inclusion h

theorem Sublattice.inclusion_apply {α : Type u_2} [Lattice α] {L M : Sublattice α} (h : L ≤ M) (a : ↥L) : (inclusion h) a = Set.inclusion h a

theorem Sublattice.inclusion_injective {α : Type u_2} [Lattice α] {L M : Sublattice α} (h : L ≤ M) : Function.Injective ⇑(inclusion h)

@[simp]

theorem Sublattice.inclusion_rfl {α : Type u_2} [Lattice α] (L : Sublattice α) : inclusion ⋯ = LatticeHom.id ↥L

@[simp]

theorem Sublattice.subtype_comp_inclusion {α : Type u_2} [Lattice α] {L M : Sublattice α} (h : L ≤ M) : M.subtype.comp (inclusion h) = L.subtype

@[implicit_reducible]

instance Sublattice.instTop {α : Type u_2} [Lattice α] : Top (Sublattice α)

The maximum sublattice of a lattice.

Equations

• Sublattice.instTop = { top := { carrier := Set.univ, supClosed' := ⋯, infClosed' := ⋯ } }

@[implicit_reducible]

instance Sublattice.instBot {α : Type u_2} [Lattice α] : Bot (Sublattice α)

The empty sublattice of a lattice.

Equations

• Sublattice.instBot = { bot := { carrier := ∅, supClosed' := ⋯, infClosed' := ⋯ } }

@[implicit_reducible]

instance Sublattice.instInf {α : Type u_2} [Lattice α] : Min (Sublattice α)

The inf of two sublattices is their intersection.

Equations

• Sublattice.instInf = { min := fun (L M : Sublattice α) => { carrier := ↑L ∩ ↑M, supClosed' := ⋯, infClosed' := ⋯ } }

@[implicit_reducible]

instance Sublattice.instInfSet {α : Type u_2} [Lattice α] : InfSet (Sublattice α)

The inf of sublattices is their intersection.

Equations

• Sublattice.instInfSet = { sInf := fun (S : Set (Sublattice α)) => { carrier := ⨅ L ∈ S, ↑L, supClosed' := ⋯, infClosed' := ⋯ } }

@[implicit_reducible]

instance Sublattice.instInhabited {α : Type u_2} [Lattice α] : Inhabited (Sublattice α)

Equations

• Sublattice.instInhabited = { default := ⊥ }

def Sublattice.topEquiv {α : Type u_2} [Lattice α] : ↥⊤ ≃o α

The top sublattice is isomorphic to the original lattice.

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

Equations

• Sublattice.topEquiv = { toEquiv := Equiv.Set.univ α, map_rel_iff' := ⋯ }

@[simp]

theorem Sublattice.coe_top {α : Type u_2} [Lattice α] : ↑⊤ = Set.univ

@[simp]

theorem Sublattice.coe_bot {α : Type u_2} [Lattice α] : ↑⊥ = ∅

@[simp]

theorem Sublattice.coe_inf' {α : Type u_2} [Lattice α] (L M : Sublattice α) : ↑(L ⊓ M) = ↑L ∩ ↑M

@[simp]

theorem Sublattice.coe_sInf {α : Type u_2} [Lattice α] (S : Set (Sublattice α)) : ↑(sInf S) = ⋂ L ∈ S, ↑L

@[simp]

theorem Sublattice.coe_iInf {ι : Sort u_1} {α : Type u_2} [Lattice α] (f : ι → Sublattice α) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

@[simp]

theorem Sublattice.coe_eq_univ {α : Type u_2} [Lattice α] {L : Sublattice α} : ↑L = Set.univ ↔ L = ⊤

@[simp]

theorem Sublattice.coe_eq_empty {α : Type u_2} [Lattice α] {L : Sublattice α} : ↑L = ∅ ↔ L = ⊥

@[simp]

theorem Sublattice.notMem_bot {α : Type u_2} [Lattice α] (a : α) : a ∉ ⊥

@[simp]

theorem Sublattice.mem_top {α : Type u_2} [Lattice α] (a : α) : a ∈ ⊤

@[simp]

theorem Sublattice.mem_inf {α : Type u_2} [Lattice α] {L M : Sublattice α} {a : α} : a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M

@[simp]

theorem Sublattice.mem_sInf {α : Type u_2} [Lattice α] {a : α} {S : Set (Sublattice α)} : a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

@[simp]

theorem Sublattice.mem_iInf {ι : Sort u_1} {α : Type u_2} [Lattice α] {a : α} {f : ι → Sublattice α} : a ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

@[implicit_reducible]

instance Sublattice.instCompleteLattice {α : Type u_2} [Lattice α] : CompleteLattice (Sublattice α)

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} [Lattice α] : Subsingleton (Sublattice α) ↔ IsEmpty α

@[implicit_reducible]

instance Sublattice.instUniqueOfIsEmpty {α : Type u_2} [Lattice α] [IsEmpty α] : Unique (Sublattice α)

Equations

• Sublattice.instUniqueOfIsEmpty = { toInhabited := Sublattice.instInhabited, uniq := ⋯ }

def Sublattice.comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice β) : Sublattice α

The preimage of a sublattice along a lattice homomorphism.

Equations

• Sublattice.comap f L = { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯ }

@[simp]

theorem Sublattice.coe_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (f : LatticeHom α β) : ↑(comap f L) = ⇑f ⁻¹' ↑L

@[simp]

theorem Sublattice.mem_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} {a : α} {L : Sublattice β} : a ∈ comap f L ↔ f a ∈ L

theorem Sublattice.comap_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} : Monotone (comap f)

@[simp]

theorem Sublattice.comap_id {α : Type u_2} [Lattice α] (L : Sublattice α) : comap (LatticeHom.id α) L = L

@[simp]

theorem Sublattice.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] (L : Sublattice γ) (g : LatticeHom β γ) (f : LatticeHom α β) : comap f (comap g L) = comap (g.comp f) L

def Sublattice.map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) : Sublattice β

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

Equations

• Sublattice.map f L = { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }

@[simp]

theorem Sublattice.coe_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) : ↑(map f L) = ⇑f '' ↑L

@[simp]

theorem Sublattice.mem_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {b : β} : b ∈ map f L ↔ ∃ a ∈ L, f a = b

theorem Sublattice.mem_map_of_mem {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) {a : α} : a ∈ L → f a ∈ map f L

theorem Sublattice.apply_coe_mem_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) (a : ↥L) : f ↑a ∈ map f L

theorem Sublattice.map_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} : Monotone (map f)

@[simp]

theorem Sublattice.map_id {α : Type u_2} [Lattice α] {L : Sublattice α} : map (LatticeHom.id α) L = L

@[simp]

theorem Sublattice.map_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] {L : Sublattice α} (g : LatticeHom β γ) (f : LatticeHom α β) : map g (map f L) = map (g.comp f) L

theorem Sublattice.mem_map_equiv {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : α ≃o β} {a : β} : a ∈ map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L ↔ f.symm a ∈ L

theorem Sublattice.apply_mem_map_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {a : α} (hf : Function.Injective ⇑f) : f a ∈ map f L ↔ a ∈ L

theorem Sublattice.map_equiv_eq_comap_symm {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : α ≃o β) (L : Sublattice α) : map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L = comap { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L

theorem Sublattice.comap_equiv_eq_map_symm {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : β ≃o α) (L : Sublattice α) : comap { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L = map { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L

theorem Sublattice.map_symm_eq_iff_eq_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} {e : β ≃o α} : map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M

theorem Sublattice.map_le_iff_le_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {M : Sublattice β} : map f L ≤ M ↔ L ≤ comap f M

theorem Sublattice.gc_map_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : GaloisConnection (map f) (comap f)

@[simp]

theorem Sublattice.map_bot {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : map f ⊥ = ⊥

theorem Sublattice.map_sup {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L M : Sublattice α) : map f (L ⊔ M) = map f L ⊔ map f M

theorem Sublattice.map_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ι → Sublattice α) : map f (⨆ (i : ι), L i) = ⨆ (i : ι), map f (L i)

@[simp]

theorem Sublattice.comap_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : comap f ⊤ = ⊤

theorem Sublattice.comap_inf {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L M : Sublattice β) (f : LatticeHom α β) : comap f (L ⊓ M) = comap f L ⊓ comap f M

theorem Sublattice.comap_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (s : ι → Sublattice β) : comap f (iInf s) = ⨅ (i : ι), comap f (s i)

theorem Sublattice.map_inf_le {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L M : Sublattice α) (f : LatticeHom α β) : map f (L ⊓ M) ≤ map f L ⊓ map f M

theorem Sublattice.le_comap_sup {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L M : Sublattice β) (f : LatticeHom α β) : comap f L ⊔ comap f M ≤ comap f (L ⊔ M)

theorem Sublattice.le_comap_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ι → Sublattice β) : ⨆ (i : ι), comap f (L i) ≤ comap f (⨆ (i : ι), L i)

theorem Sublattice.map_inf {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L M : Sublattice α) (f : LatticeHom α β) (hf : Function.Injective ⇑f) : map f (L ⊓ M) = map f L ⊓ map f M

theorem Sublattice.map_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (h : Function.Surjective ⇑f) : map f ⊤ = ⊤

def Sublattice.prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) : Sublattice (α × β)

Binary product of sublattices as a sublattice.

Equations

• L.prod M = { carrier := ↑L ×ˢ ↑M, supClosed' := ⋯, infClosed' := ⋯ }

@[simp]

theorem Sublattice.coe_prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) : ↑(L.prod M) = ↑L ×ˢ ↑M

@[simp]

theorem Sublattice.mem_prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} {p : α × β} : p ∈ L.prod M ↔ p.1 ∈ L ∧ p.2 ∈ M

theorem Sublattice.prod_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L₁ L₂ : Sublattice α} {M₁ M₂ : Sublattice β} (hL : L₁ ≤ L₂) (hM : M₁ ≤ M₂) : L₁.prod M₁ ≤ L₂.prod M₂

theorem Sublattice.prod_mono_left {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L₁ L₂ : Sublattice α} {M : Sublattice β} (hL : L₁ ≤ L₂) : L₁.prod M ≤ L₂.prod M

theorem Sublattice.prod_mono_right {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M₁ M₂ : Sublattice β} (hM : M₁ ≤ M₂) : L.prod M₁ ≤ L.prod M₂

theorem Sublattice.prod_left_mono {α : Type u_2} [Lattice α] {M : Sublattice α} : Monotone fun (L : Sublattice α) => L.prod M

theorem Sublattice.prod_right_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} : Monotone fun (M : Sublattice β) => L.prod M

theorem Sublattice.prod_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) : L.prod ⊤ = comap LatticeHom.fst L

theorem Sublattice.top_prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) : ⊤.prod L = comap LatticeHom.snd L

@[simp]

theorem Sublattice.top_prod_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] : ⊤.prod ⊤ = ⊤

@[simp]

theorem Sublattice.prod_bot {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) : L.prod ⊥ = ⊥

@[simp]

theorem Sublattice.bot_prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (M : Sublattice β) : ⊥.prod M = ⊥

theorem Sublattice.le_prod_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} {N : Sublattice (α × β)} : N ≤ L.prod M ↔ N ≤ comap LatticeHom.fst L ∧ N ≤ comap LatticeHom.snd M

@[simp]

theorem Sublattice.prod_eq_bot {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} : L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥

@[simp]

theorem Sublattice.prod_eq_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} [Nonempty α] [Nonempty β] {M : Sublattice β} : L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤

def Sublattice.prodEquiv {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) : ↥(L.prod M) ≃o ↥L × ↥M

The product of sublattices is isomorphic to their product as lattices.

Equations

• L.prodEquiv M = { toEquiv := Equiv.Set.prod ↑L ↑M, map_rel_iff' := ⋯ }

@[simp]

theorem Sublattice.prodEquiv_symm_apply {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) (x : { a : α // (fun (x : α) => x ∈ ↑L) a } × { b : β // (fun (x : β) => x ∈ ↑M) b }) : (RelIso.symm (L.prodEquiv M)) x = ⟨(↑x.1, ↑x.2), ⋯⟩

@[simp]

theorem Sublattice.prodEquiv_apply {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) (x : { c : α × β // (fun (x : α) => x ∈ ↑L) c.1 ∧ (fun (x : β) => x ∈ ↑M) c.2 }) : (L.prodEquiv M) x = (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩)

@[simp]

theorem Sublattice.prodEquiv_toEquiv {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) : (L.prodEquiv M).toEquiv = Equiv.Set.prod ↑L ↑M

def Sublattice.pi {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] (s : Set κ) (L : (i : κ) → Sublattice (π i)) : Sublattice ((i : κ) → π i)

Arbitrary product of sublattices. Given an index set s and a family of sublattices L : Π i, Sublattice (α i), pi s L is the sublattice of dependent functions f : Π i, α i such that f i belongs to L i whenever i ∈ s.

Equations

• Sublattice.pi s L = { carrier := s.pi fun (i : κ) => ↑(L i), supClosed' := ⋯, infClosed' := ⋯ }

@[simp]

theorem Sublattice.coe_pi {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] (s : Set κ) (L : (i : κ) → Sublattice (π i)) : ↑(pi s L) = s.pi fun (i : κ) => ↑(L i)

@[simp]

theorem Sublattice.mem_pi {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] {s : Set κ} {L : (i : κ) → Sublattice (π i)} {x : (i : κ) → π i} : x ∈ pi s L ↔ ∀ i ∈ s, x i ∈ L i

@[simp]

theorem Sublattice.pi_empty {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] (L : (i : κ) → Sublattice (π i)) : pi ∅ L = ⊤

@[simp]

theorem Sublattice.pi_top {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] (s : Set κ) : (pi s fun (x : κ) => ⊤) = ⊤

@[simp]

theorem Sublattice.pi_bot {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] {s : Set κ} (hs : s.Nonempty) : (pi s fun (x : κ) => ⊥) = ⊥

theorem Sublattice.pi_univ_bot {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] [Nonempty κ] : (pi Set.univ fun (x : κ) => ⊥) = ⊥

theorem Sublattice.le_pi {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] {s : Set κ} {L : (i : κ) → Sublattice (π i)} {M : Sublattice ((i : κ) → π i)} : M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom i) (L i)

@[simp]

theorem Sublattice.pi_univ_eq_bot_iff {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] {L : (i : κ) → Sublattice (π i)} : pi Set.univ L = ⊥ ↔ ∃ (i : κ), L i = ⊥

theorem Sublattice.pi_univ_eq_bot {κ : Type u_5} {π : κ → Type u_6} [(i : κ) → Lattice (π i)] {L : (i : κ) → Sublattice (π i)} {i : κ} (hL : L i = ⊥) : pi Set.univ L = ⊥