conditionallyCompleteLattice — Mathlib

Lean4
instance conditionallyCompleteLattice {ι : Type*} {α : ι → Type*} [∀ i, ConditionallyCompleteLattice (α i)] :
    ConditionallyCompleteLattice (∀ i, α i) :=
  { Pi.instLattice, Pi.supSet,
    Pi.infSet with
    le_csSup := fun _ f ⟨g, hg⟩ hf i => le_csSup ⟨g i, Set.forall_mem_range.2 fun ⟨_, hf'⟩ => hg hf' i⟩ ⟨⟨f, hf⟩, rfl⟩
    csSup_le := fun s _ hs hf i =>
      (csSup_le (by haveI := hs.to_subtype; apply range_nonempty)) fun _ ⟨⟨_, hg⟩, hb⟩ => hb ▸ hf hg i
    csInf_le := fun _ f ⟨g, hg⟩ hf i => csInf_le ⟨g i, Set.forall_mem_range.2 fun ⟨_, hf'⟩ => hg hf' i⟩ ⟨⟨f, hf⟩, rfl⟩
    le_csInf := fun s _ hs hf i =>
      (le_csInf (by haveI := hs.to_subtype; apply range_nonempty)) fun _ ⟨⟨_, hg⟩, hb⟩ => hb ▸ hf hg i }
Похожие утверждения