Ico_diff_Iio

Mathlib.Order.Interval.Set.LinearOrder

URI: https://scilib.ai/kg/mathlib#Set.Ico_diff_Iio

English

For a ≤ b and c in α, the difference [a, b) \ (-∞, c) equals [max(a, c), b).

Русский

Для a ≤ b и любого c: [a, b) \ (-∞, c) = [max(a, c), b).

LaTeX

$$$Ico(a,b) \\\\ Iio(c) = Ico(\\\\max(a,c), b)$$$

Lean4

@[simp]
theorem Ico_diff_Iio : Ico a b \ Iio c = Ico (max a c) b := by rw [diff_eq, compl_Iio, Ico_inter_Ici]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru