subset_infClosure

Mathlib.Order.SupClosed

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

English

s is contained in its infClosure: s ⊆ infClosure(s).

Русский

s ⊆ infClosure(s).

LaTeX

$$$s \\subseteq \\operatorname{infClosure}(s)$$$

Lean4

@[simp]
theorem subset_infClosure {s : Set α} : s ⊆ infClosure s :=
  infClosure.le_closure _

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

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

Разделы

Аффилиация

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