instLocallyFiniteOrderBot — Mathlib

English

The half-open interval from a left-injection to a right-injection is empty: Ioc(inl a1, inr b2) = ∅.

Русский

Полуоткрытый интервал между левым и правым вложениями пуст.

LaTeX

$$$\mathrm{Ioc}(\mathrm{inl}(a_1),\mathrm{inr}(b_2)) = \emptyset$$$

Lean4

instance : LocallyFiniteOrderBot (α ⊕ β)
    where
  finsetIic := Sum.elim (Iic · |>.map .inl) (Iic · |>.map .inr)
  finsetIio := Sum.elim (Iio · |>.map .inl) (Iio · |>.map .inr)
  finset_mem_Iic := by simp
  finset_mem_Iio := by simp

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