toIsStronglyAtomic — Mathlib

English

In a SuccOrder, for any a < b, a is strongly atomic relative to b, with succ(a) as a witness.

Русский

В порядке SuccOrder для любых a < b существует свидетельство того, что a — сильно атомарно, через succ(a).

LaTeX

$$$ [SuccOrder\ α] \Rightarrow [IsStronglyAtomic α] \Rightarrow \forall a,b (a < b) \rightarrow \exists x (a \prec x) \land x \le b $$$

Lean4

instance toIsStronglyAtomic [SuccOrder α] : IsStronglyAtomic α where
  exists_covBy_le_of_lt a _
    hab := ⟨SuccOrder.succ a, Order.covBy_succ_of_not_isMax fun ha ↦ ha.not_lt hab, SuccOrder.succ_le_of_lt hab⟩

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