Icc_subset_Iio_iff

Mathlib.Order.Interval.Set.Basic

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

English

Suppose a1 ≤ b1. Then Icc(a1,b1) ⊆ Iio(b2) holds if and only if b1 < b2.

Русский

Пусть a1 ≤ b1. Тогда Icc(a1,b1) ⊆ Iio(b2) эквивалентно b1 < b2.

LaTeX

$$$$Icc(a_1,b_1) \subseteq Iio(b_2) \iff b_1 < b_2$$$$

Lean4

theorem Icc_subset_Iio_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Iio b₂ ↔ b₁ < b₂ :=
  ⟨fun h => h ⟨h₁, le_rfl⟩, fun h _ ⟨_, hx'⟩ => hx'.trans_lt h⟩

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

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

Разделы

Аффилиация

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