English
In Set.Iic b, an element a is a coatom iff its underlying value is a coatom in the ambient order with top b.
Русский
В Set.Iic(b) элемент a является коатомом тогда, когда его основанное значение является коатомом в исходном порядке с верхом b.
LaTeX
$$$ \\forall {b}, \\forall {a : (Set.Iic b).Elem}, \\mathrm{IsCoatom}(a) \\iff \\mathrm{CovBy}(a.{val}, b).$$$
Lean4
@[simp]
theorem isCoatom_iff {a : Set.Iic b} : IsCoatom a ↔ ↑a ⋖ b :=
by
rw [← covBy_top_iff]
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Iic
