subset_lowerClosure

Mathlib.Order.UpperLower.Closure

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

English

s ⊆ lowerClosure s for any s.

Русский

для любого s выполняется s ⊆ lowerClosure s.

LaTeX

$$s ⊆ lowerClosure s$$

Lean4

theorem subset_lowerClosure : s ⊆ lowerClosure s := fun x hx => ⟨x, hx, le_rfl⟩

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

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

Разделы

Аффилиация

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