subset_upperClosure

Mathlib.Order.UpperLower.Closure

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

English

s ⊆ upperClosure s for any s.

Русский

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

LaTeX

$$s ⊆ upperClosure s$$

Lean4

theorem subset_upperClosure : s ⊆ upperClosure s := fun x hx => ⟨x, hx, le_rfl⟩

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

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

Разделы

Аффилиация

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