Ico_subset_Ico_right

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.Ico_subset_Ico_right

English

If b1 ≤ b2, then Ico(a,b1) ⊆ Ico(a,b2).

Русский

Если b1 ≤ b2, то Ico(a,b1) ⊆ Ico(a,b2).

LaTeX

$$b_1 \le b_2 \Rightarrow Ico(a,b_1) \subseteq Ico(a,b_2)$$

Lean4

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

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

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

Разделы

Аффилиация

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