mem_cast

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.mem_cast

English

Membership is preserved under cast: a ∈ Sym.cast h s iff a ∈ s.

Русский

Членство сохраняется при приводлении: a ∈ Sym.cast h s ⇔ a ∈ s.

LaTeX

$$$ a \\in \\mathrm{Sym.cast}\\, h\\, s \\;\\iff\\; a \\in s$$$

Lean4

@[simp]
theorem mem_cast (h : n = m) : a ∈ Sym.cast h s ↔ a ∈ s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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