Ico_bot — Mathlib

English

In a dense preorder α with bottom ⊥, the half-open interval [⊥, a) equals the open-interval (−∞, a).

Русский

В плотном предопорядке α с нижней границей ⊥ полуоткрытый интервал [⊥, a) совпадает с открытым интервалом (−∞, a).

LaTeX

$$$\{ x \in \alpha \mid \bot \le x < a \} = \{ x \in \alpha \mid x < a \}$$$

Lean4

@[simp]
theorem Ico_bot : Ico ⊥ a = Iio a := by simp [← Ici_inter_Iio]

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