Ioo_subset_Ioo

Mathlib.Order.Interval.Finset.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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