isStronglyCoatomic — Mathlib

English

If α is strongly coatomic, and s is OrdConnected, then s.Elem is strongly coatomic.

Русский

Если α сильно коатомно, и s OrdConnected, то s.Elem сильно коатомно.

LaTeX

$$$ [IsStronglyCoatomic α] \to [Set.OrdConnected s] \to IsStronglyCoatomic s.Elem $$$

Lean4

theorem isStronglyCoatomic [IsStronglyCoatomic α] {s : Set α} (h : Set.OrdConnected s) : IsStronglyCoatomic s :=
  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 h.dual.isStronglyAtomic

Похожие утверждения