Ico_subset_Ico_left

Mathlib.Order.Interval.Set.Basic

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

English

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

Русский

Пусть α — упорядоченное множество. Если a₁ ≤ a₂, то Ico(a₂, b) ⊆ Ioo(a₁, b).

LaTeX

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

Lean4

theorem Ico_subset_Ico_left (h : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b :=
  Ico_subset_Ico h le_rfl

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

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

Разделы

Аффилиация

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