Iic_inter_Ici — Mathlib

English

Let α be a type with a preorder. Then Iic a ∩ Ici b = Icc b a, i.e., the intersection of {x | x ≤ a} and {x | a ≤ x} equals {x | b ≤ x ≤ a}.

Русский

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

LaTeX

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

Lean4

theorem Iic_inter_Ici : Iic a ∩ Ici b = Icc b a :=
  inter_comm _ _

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