subset_closure

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.subset_closure

English

A set is contained in its closure: s ⊆ closure L s.

Русский

Множество содержится в своем замыкании: s ⊆ closure_L(s).

LaTeX

$$$$ s \subseteq closure L s $$$$

Lean4

/-- The substructure generated by a set includes the set. -/
@[simp]
theorem subset_closure : s ⊆ closure L s :=
  (closure L).le_closure s

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

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

Разделы

Аффилиация

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