infClosure_min

Mathlib.Order.SupClosed

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

English

If s ⊆ t and InfClosed t, then infClosure(s) ⊆ t.

Русский

Если s ⊆ t и tInf является InfClosed, тогда infClosure(s) ⊆ t.

LaTeX

$$$s \subseteq t \to InfClosed\, t \to \infClosure s \subseteq t$$$

Lean4

theorem infClosure_min : s ⊆ t → InfClosed t → infClosure s ⊆ t :=
  infClosure.closure_min

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

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

Разделы

Аффилиация

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