upperClosure_min

Mathlib.Order.UpperLower.Closure

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

English

If s ⊆ t and t is an upper set, then upperClosure s ⊆ t.

Русский

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

LaTeX

$$(s ⊆ t) ∧ IsUpperSet(t) → upperClosure s ⊆ t$$

Lean4

theorem upperClosure_min (h : s ⊆ t) (ht : IsUpperSet t) : ↑(upperClosure s) ⊆ t := fun _a ⟨_b, hb, hba⟩ =>
  ht hba <| h hb

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

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

Разделы

Аффилиация

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