Icc_subset_Icc

Mathlib.Order.Interval.Finset.Basic

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

English

If a2 ≤ a1 and b1 ≤ b2, then Icc(a1,b1) ⊆ Icc(a2,b2).

Русский

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

LaTeX

$$a_2 \le a_1 \land b_1 \le b_2 \Rightarrow Icc(a_1,b_1) \subseteq Icc(a_2,b_2)$$

Lean4

@[gcongr]
theorem Icc_subset_Icc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Icc a₂ b₂ := by
  simpa [← coe_subset] using Set.Icc_subset_Icc ha hb

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

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

Разделы

Аффилиация

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