English
In a strongly coatomic poset, if (Iic a) is infinite and { x | x ⋖ a } is finite, then there exists b with b ⋖ a and (Iic b) is infinite.
Русский
В сильно коатомном частично упорядоченном множестве, если (Iic a) бесконечно и { x | x ⋖ a } конечно, то существует b, что b ⋖ a и (Iic b) бесконечно.
LaTeX
$$$[IsStronglyCoatomic]\\ α \\rightarrow (\\operatorname{Iic} a).Infinite \\land \\{x \\mid x \\prec a\\}.Finite \\rightarrow \\exists b\\, (b \\prec a) \\land (\\operatorname{Iic} b).Infinite.$$$
Lean4
theorem exists_covby_infinite_Iic_of_infinite_Iic [IsStronglyCoatomic α] (ha : (Set.Iic a).Infinite)
(hfin : {x | x ⋖ a}.Finite) : ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite :=
by
simp_rw [← toDual_covBy_toDual_iff (α := α)] at hfin ⊢
exact exists_covby_infinite_Ici_of_infinite_Ici (α := αᵒᵈ) ha hfin
