English
In a complete lattice, an element k is compact iff whenever a directed family has supremum above k, some member of the family already lies above k.
Русский
В полной решётке элемент k компакт iff всякий направляемый набор с верхой сверху k содержит элемент, выше k.
LaTeX
$$CompleteLattice.IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s$$
Lean4
theorem isCompactElement_iff.{u} {α : Type u} [CompleteLattice α] (k : α) :
CompleteLattice.IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s := by
classical
constructor
· intro H ι s hs
obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
choose f hf using this
refine ⟨Finset.univ.image f, ht'.trans ?_⟩
rw [Finset.sup_le_iff]
intro b hb
rw [← show s (f ⟨b, hb⟩) = id b from hf _]
exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
· intro H s hs
obtain ⟨t, ht⟩ :=
H s Subtype.val
(by
delta iSup
rwa [Subtype.range_coe])
refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
rw [Finset.sup_le_iff]
exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
