Ioo_subset_Ioo_left

Mathlib.Order.Interval.Set.Basic

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

English

Let α be a preorder. If a₁ ≤ a₂, then Ioo(a₂, b) ⊆ Ioo(a₁, b).

Русский

Пусть α — упорядоченный по крайней мере до допускающее множество. Если a₁ ≤ a₂, то (a₂, b) ⊆ (a₁, b).

LaTeX

$$$a_1 \le a_2 \Rightarrow Ioo(a_2,b) \subseteq Ioo(a_1,b)$$$

Lean4

theorem Ioo_subset_Ioo_left (h : a₁ ≤ a₂) : Ioo a₂ b ⊆ Ioo a₁ b :=
  Ioo_subset_Ioo h le_rfl

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

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

Разделы

Аффилиация

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