Ici_subset_Ioi_pred_of_not_isMin — Mathlib

English

If a is not a minimal element, then every x with a ≤ x satisfies pred a < x.

Русский

Если a не минимален, то для любого x с a ≤ x выполняется pred a < x.

LaTeX

$$$$\forall a \colon \alpha, \neg IsMin(a) \Rightarrow \{ x \in \alpha \mid a \le x \} \subseteq \{ x \in \alpha \mid pred(a) < x \}.$$$$

Lean4

theorem Ici_subset_Ioi_pred_of_not_isMin (ha : ¬IsMin a) : Ici a ⊆ Ioi (pred a) := fun _ ↦ pred_lt_of_not_isMin_of_le ha

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