Iio_subset_Iic

Mathlib.Order.Interval.Set.Basic

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

← MathLib Explorer

English

If a ≤ b, then (-∞, a) ⊆ (-∞, b].

Русский

Если a ≤ b, то (-∞, a) ⊆ (-∞, b].

LaTeX

$$$$Iio(a) \subseteq Iic(b)$$$$

Lean4

/-- If `a ≤ b`, then `(-∞, a) ⊆ (-∞, b]`. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use `Iio_subset_Iic_iff`. -/
theorem Iio_subset_Iic (h : a ≤ b) : Iio a ⊆ Iic b :=
  Subset.trans (Iio_subset_Iio h) Iio_subset_Iic_self

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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