Ioi_inter_Iic — 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-closed ray {x ∈ α | x ≤ b} equals the half-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 \le b \} = \{ x \in \alpha \mid a < x \le b \} $$$$

Lean4

theorem Ioi_inter_Iic : Ioi a ∩ Iic b = Ioc a b :=
  rfl

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