English
In a complete lattice, having a sequence with p-satisfied and top as supremum is equivalent to having a countable set of p-satisfying elements with top as supremum.
Русский
В полном положеении существование последовательности, достигающей верхнего предела, эквивалентно существованию счетного множества элементов, удовлетворяющих условию, с тем же верхом.
LaTeX
$$$\\text{exists_seq_iSup_eq_top_iff_countable} \\ [\\text{CompleteLattice}\\,\\alpha] \\{p:\\alpha\\to\\operatorname{Prop}\\} (h:\\exists x, p\\,x) : \\left(\\exists s:\\mathbb{N}\\to \\alpha, (\\forall n, p(s(n))) \\land (\\bigvee_{n} s(n)) = \\top\\right) \\iff \\left(\\exists S:\\Set\\alpha, S.Countable \\land (\\forall s\\in S, p\\,s) \\land \\operatorname{sSup}(S) = \\top\\right)$$$$
Lean4
theorem exists_seq_iSup_eq_top_iff_countable [CompleteLattice α] {p : α → Prop} (h : ∃ x, p x) :
(∃ s : ℕ → α, (∀ n, p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S : Set α, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤ :=
by
constructor
· rintro ⟨s, hps, hs⟩
refine ⟨range s, countable_range s, forall_mem_range.2 hps, ?_⟩
rwa [sSup_range]
· rintro ⟨S, hSc, hps, hS⟩
rcases eq_empty_or_nonempty S with (rfl | hne)
· rw [sSup_empty] at hS
haveI := subsingleton_of_bot_eq_top hS
rcases h with ⟨x, hx⟩
exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
· rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩
rwa [hs.iSup_comp, ← sSup_eq_iSup']
