Iio_inter_Ici — Mathlib

English

Let α be a type with a preorder. Then Iio a ∩ Ici b = Ico b a, i.e., {x | x < a} ∩ {x | b ≤ x} = {x | b ≤ x < a}.

Русский

Пусть α — множество с порядком. Тогда Iio a ∩ Ici b = Ico b a, т.е. {x | x < a} ∩ {x | b ≤ x} = {x | b ≤ x < a}.

LaTeX

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

Lean4

theorem Iio_inter_Ici : Iio a ∩ Ici b = Ico b a :=
  inter_comm _ _

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