Documentation

🔶 coverage

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

Instances For

@[implicit_reducible]

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

SetLike (Sublattice α) α

@[implicit_reducible]

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

PartialOrder (Sublattice α)

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

Set α

See Note [custom simps projection].

Instances For

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

Instances For

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.

Instances For

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

@[implicit_reducible]

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

Min ↥L

A sublattice of a lattice inherits an infimum.

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

@[implicit_reducible]

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

DistribLattice ↥L

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

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

LatticeHom (↥L) α

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

Instances For

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

Instances For

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

@[implicit_reducible]

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

Bot (Sublattice α)

The empty sublattice of a lattice.

@[implicit_reducible]

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

Min (Sublattice α)

The inf of two sublattices is their intersection.

@[implicit_reducible]

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

InfSet (Sublattice α)

The inf of sublattices is their intersection.

@[implicit_reducible]

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

Inhabited (Sublattice α)

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

Instances For

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

theorem Sublattice.subsingleton_iff {α : Type u_2} [Lattice α] :

Subsingleton (Sublattice α) ↔ IsEmpty α

@[implicit_reducible]

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

Unique (Sublattice α)

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.

Instances For

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

Instances For

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

Instances For

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

Instances For

@[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_toEquiv {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice β) :

(L.prodEquiv M).toEquiv = Equiv.Set.prod ↑L ↑M

@[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, ⋯⟩)

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.

Instances For

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