restrict_of_mem

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.restrict_of_mem

English

If a ∈ S, then S.restrict a = ⟨a, a∈S⟩.

Русский

Если a ∈ S, то ограничение S.restrict a равно ⟨a, доказательство принадлежности⟩.

LaTeX

$$$(ha : a \in S) : S.restrict(a) = \langle a, ha\rangle$$$

Lean4

@[simp]
theorem restrict_of_mem (ha : a ∈ S) : S.restrict a = ⟨a, ha⟩ :=
  S.giRestrict.l_u_eq ⟨a, ha⟩

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

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

Разделы

Аффилиация

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