English
An element k is compact iff for every nonempty directed subset s, if k ≤ sup s then there exists x ∈ s with k ≤ x.
Русский
Элемент k компакт iff для всякого ненулевого направленного подмножества s, если k ≤ sup s, существует x ∈ s такой, что k ≤ x.
LaTeX
$$IsCompactElement k ↔ ∀ s : Set α, s.Nonempty → DirectedOn (≤) s → k ≤ sSup s → ∃ x : α, x ∈ s ∧ k ≤ x$$
Lean4
/-- An element `k` is compact if and only if any directed set with `sSup` above
`k` already got above `k` at some point in the set. -/
theorem isCompactElement_iff_le_of_directed_sSup_le (k : α) :
IsCompactElement k ↔ ∀ s : Set α, s.Nonempty → DirectedOn (· ≤ ·) s → k ≤ sSup s → ∃ x : α, x ∈ s ∧ k ≤ x := by
classical
constructor
· intro hk s hne hdir hsup
obtain ⟨t, ht⟩ := hk s hsup
have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
· intro hk s hsup
let S : Set α :=
{x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id}
-- S is directed, nonempty, and still has sup above k.
have dir_US : DirectedOn (· ≤ ·) S := by
rintro x ⟨c, hc⟩ y ⟨d, hd⟩
use x ⊔ y
constructor
· use c ∪ d
constructor
· simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
· simp only [hc.right, hd.right, Finset.sup_union]
simp only [and_self_iff, le_sup_left, le_sup_right]
have sup_S : sSup s ≤ sSup S := by
apply sSup_le_sSup
intro x hx
use { x }
simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true, Finset.sup_singleton, Set.singleton_subset_iff]
have Sne : S.Nonempty := by
suffices ⊥ ∈ S from Set.nonempty_of_mem this
use ∅
simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, and_self_iff]
-- Now apply the defn of compact and finish.
obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
use t
exact ⟨htS, by rwa [← htsup]⟩
