Iic_inter_Ioi — Mathlib

English

Let α be a type with a preorder. Then Iic a ∩ Ioi b = Ioc b a, i.e., {x | x ≤ a} ∩ {x | b < x} = {x | b < x ≤ a}.

Русский

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

LaTeX

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

Lean4

theorem Iic_inter_Ioi : Iic a ∩ Ioi b = Ioc b a :=
  inter_comm _ _

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