bot_lt_iff_ne_bot — Mathlib

English

Bottom is strictly less than x in WithBot α if and only if x is not bottom.

Русский

Нижний элемент строго меньше x в WithBot α тогда и только тогда, когда x не является нижним.

LaTeX

$$$ \bot < x \iff x \neq \bot $$$

Lean4

/-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
`PartialOrder α`. -/
protected theorem bot_lt_iff_ne_bot : ⊥ < x ↔ x ≠ ⊥ := by cases x <;> simp

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