English
In a strongly atomic poset, if (Ici a) is infinite and { x | a ⋖ x } is finite, then there exists b with a ⋖ b and (Ici b) is infinite.
Русский
В сильно атомарном частично упорядоченном множестве, если (Ici a) бесконечно и { x | a ⋖ x } конечно, то существует b such that a ⋖ b и (Ici b) бесконечно.
LaTeX
$$$(\\operatorname{Ici} a).Infinite \\land \\{x \\mid a \\prec x\\}.Finite \\rightarrow \\exists b\\, (a \\prec b) \\land (\\operatorname{Ici} b).Infinite.$$$
Lean4
theorem exists_covby_infinite_Ici_of_infinite_Ici [IsStronglyAtomic α] (ha : (Set.Ici a).Infinite)
(hfin : {x | a ⋖ x}.Finite) : ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite :=
by
by_contra! h
refine
((hfin.biUnion (t := Set.Ici) (by simpa using h)).subset (fun b hb ↦ ?_)).not_infinite
(ha.diff (Set.finite_singleton a))
obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le
exact Set.mem_biUnion hax hxb
