Ioi_subset

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#IsUpperSet.Ioi_subset

English

If s is upper and a ∈ s, then Ioi a ⊆ s.

Русский

Если s — верхнее множество и a ∈ s, то Ioi a ⊆ s.

LaTeX

$$$IsUpperSet s \\to \\forall a\\in s, Ioi a \\subseteq s$$$

Lean4

theorem Ioi_subset (h : IsUpperSet s) ⦃a⦄ (ha : a ∈ s) : Ioi a ⊆ s :=
  Ioi_subset_Ici_self.trans <| h.Ici_subset ha

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

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

Разделы

Аффилиация

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