English
Let K be an element of a SetLike object with top. Then IsCoatom(K) holds iff K ≠ ⊤ and for all H,g, if K ≤ H and g ∉ K then g ∈ H implies H = ⊤.
Русский
Пусть K принадлежит множеству SetLike с верхом. Тогда IsCoatom(K) равносильно K ≠ ⊤ и для всех H,g, если K ≤ H и g ∉ K, то g ∈ H влечёт H = ⊤.
LaTeX
$$$ \\mathrm{IsCoatom}(K) \\iff \\big(K \\neq \\top \\land \\forall H\\, g,\\ K \\le H \\to g \\notin K \\to g \\in H \\to H = \\top\\big).$$$
Lean4
theorem isCoatom_iff [OrderTop A] {K : A} : IsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤ := by
simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists, and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp,
and_comm]
