Icc_subset_Ioi_iff

Mathlib.Order.Interval.Set.Basic

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

English

Let a1 ≤ b1. Then Icc(a1,b1) ⊆ Ioi(a2) iff a2 < a1.

Русский

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

LaTeX

$$$$Icc(a_1,b_1) \subseteq Ioi(a_2) \iff a_2 < a_1$$$$

Lean4

theorem Icc_subset_Ioi_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁ :=
  ⟨fun h => h ⟨le_rfl, h₁⟩, fun h _ ⟨hx, _⟩ => h.trans_le hx⟩

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

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

Разделы

Аффилиация

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