covBy_iff_Ioo_eq

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#covBy_iff_Ioo_eq

English

A is covered by B if and only if A < B and Ioo A B = ∅.

Русский

A ⋖ B эквивалентно A < B и Ioo A B = ∅.

LaTeX

$$$ a \\,⋖\\, b \\iff (a < b) \\land (Ioo\\,a\\,b = \\emptyset) $$$

Lean4

theorem covBy_iff_Ioo_eq : a ⋖ b ↔ a < b ∧ Ioo a b = ∅ :=
  and_congr_right' <| by simp [eq_empty_iff_forall_notMem]

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

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

Разделы

Аффилиация

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