English
Let α be a type with a preorder. For any a,b ∈ α, the intersection of the left-closed ray {x ∈ α | a ≤ x} and the left-open 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}. Формально: {x ∈ α | a ≤ x} ∩ {x ∈ α | x < b} = {x ∈ α | a ≤ x < b}.
LaTeX
$$$$ \{ x \in \alpha \mid a \le x \} \cap \{ x \in \alpha \mid x < b \} = \{ x \in \alpha \mid a \le x < b \} $$$$
Lean4
theorem Ici_inter_Iio : Ici a ∩ Iio b = Ico a b :=
rfl
