English
In a WellFoundedGT α, any sSupIndep set s is finite.
Русский
В WellFoundedGT α любая параллельно независимая множина s конечна.
LaTeX
$$finite_of_sSupIndep [WellFoundedGT α] {s : Set α} (hs : sSupIndep s) : s.Finite$$
Lean4
theorem finite_of_sSupIndep [WellFoundedGT α] {s : Set α} (hs : sSupIndep s) : s.Finite := by
classical
refine Set.not_infinite.mp fun contra => ?_
obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t :=
by
have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
replace hs : x ⊓ sSup s = ⊥ :=
by
have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ { x } ≤ s) (by simp : x ∈ _)
simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
apply hx₁
rw [← hs, eq_comm, inf_eq_left]
exact le_sSup hx₀
