Iio_inter_Ioo — Mathlib

English

Let α be a linearly ordered set and a, b, c ∈ α. Then the intersection of the intervals (-∞, a) and (b, c) is the interval (b, min(a, c)).

Русский

Пусть α — линейно упорядоченное множество и a, b, c ∈ α. Тогда пересечение интервалов (-∞, a) и (b, c) равно (b, min(a, c)).

LaTeX

$$$Iio a \\\\cap Ioo b c = Ioo b (\\\\min a c)$$$

Lean4

theorem Iio_inter_Ioo : Iio a ∩ Ioo b c = Ioo b (min a c) := by rw [Set.inter_comm, Set.Ioo_inter_Iio, min_comm]

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