isStronglyAtomic — Mathlib

English

If α is strongly atomic, and s is an OrdConnected subset, then the induced subposet s.Elem is strongly atomic.

Русский

Если α сильно атомарно, и s — OrdConnected множество, то подструктура s.Elem сильно атомарна.

LaTeX

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

Lean4

theorem isStronglyAtomic [IsStronglyAtomic α] {s : Set α} (h : Set.OrdConnected s) : IsStronglyAtomic s where
  exists_covBy_le_of_lt := by
    rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
    obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le
    exact
      ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
        ⟨by simpa using hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using hy) (by simpa using hy')⟩, hxd⟩

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