ofEquiv_val

Mathlib.Data.Analysis.Topology

URI: https://scilib.ai/kg/mathlib#Ctop.ofEquiv_val

English

Mimics the evaluation for the mk constructor in Ctop.

Русский

Повторно описывает вычисление конструктора mk в Ctop.

LaTeX

$$$(Ctop.mk\\; f\\; T\\; \\dots ).a = f a$$$

Lean4

@[simp]
theorem ofEquiv_val (E : σ ≃ τ) (F : Ctop α σ) (a : τ) : F.ofEquiv E a = F (E.symm a) := by cases F; rfl

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

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

Разделы

Аффилиация

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