Ioi_inter_Iio — Mathlib

English

Let α be a type with a preorder. For any a,b ∈ α, the intersection of the right-open ray {x ∈ α | a < x} and the left-open ray {x ∈ α | x < b} equals the open interval {x ∈ α | a < x < b}. In symbols: {x ∈ α | a < x} ∩ {x ∈ α | x < b} = {x ∈ α | a < x < b}.

Русский

Пусть α — множество с порядком. Для любых a,b ∈ α пересечение лучей {x | a < x} и {x | x < b} есть открытый интервал {x | a < x < b}.

LaTeX

$$$$ \{ x \in \alpha \mid a < x \} \cap \{ x \in \alpha \mid x < b \} = \{ x \in \alpha \mid a < x < b \} $$$$

Lean4

theorem Ioi_inter_Iio : Ioi a ∩ Iio b = Ioo a b :=
  rfl

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