lowerClosure_min

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#lowerClosure_min

English

If s ⊆ t and t is a lower set, then lowerClosure s ⊆ t.

Русский

Если s ⊆ t и t — нижнее множество, то lowerClosure s ⊆ t.

LaTeX

$$(s ⊆ t) ∧ IsLowerSet(t) → lowerClosure s ⊆ t$$

Lean4

theorem lowerClosure_min (h : s ⊆ t) (ht : IsLowerSet t) : ↑(lowerClosure s) ⊆ t := fun _a ⟨_b, hb, hab⟩ =>
  ht hab <| h hb

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

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

Разделы

Аффилиация

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