nonempty_Ico — Mathlib

English

Let α be a preorder. The half-open interval Ico a b is nonempty exactly when a < b.

Русский

Пусть α — предпорядок. Полуоткрытый интервал Ico a b непуст тогда и только тогда, когда a < b.

LaTeX

$$$$ (\\mathrm{Ico}\\ a\\ b).\\mathrm{Nonempty} \\iff a < b. $$$$

Lean4

@[simp]
theorem nonempty_Ico : (Ico a b).Nonempty ↔ a < b :=
  ⟨fun ⟨_, hx⟩ => hx.1.trans_lt hx.2, fun h => ⟨a, left_mem_Ico.2 h⟩⟩

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