unbotD_le_iff — Mathlib

English

If x is not bottom, the comparison x.unbotD a < b is equivalent to x < b, under the appropriate auxiliary condition.

Русский

Если x не является нижним элементом, то сравнение x.unbotD a < b эквивалентно x < b при заданном условии.

LaTeX

$$$ ( \operatorname{hx} : x = \bot \rightarrow a < b ) \rightarrow ( x.unbotD a < b \iff x < b ) $$$

Lean4

theorem unbotD_le_iff (hx : x = ⊥ → a ≤ b) : x.unbotD a ≤ b ↔ x ≤ b := by cases x <;> simp [hx]

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