Icc_subset_Icc_left

Mathlib.Order.Interval.Finset.Basic

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

English

If a1 ≤ a2, then Icc(a2,b) ⊆ Icc(a1,b).

Русский

Если a1 ≤ a2, то Icc(a2,b) ⊆ Icc(a1,b).

LaTeX

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

Lean4

theorem Icc_subset_Icc_left (h : a₁ ≤ a₂) : Icc a₂ b ⊆ Icc a₁ b :=
  Icc_subset_Icc h le_rfl

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

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

Разделы

Аффилиация

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