map_proj

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.map_proj

English

For cond and x, map(f,cond)(A.proj(x)) = B.proj(f(x)).

Русский

Для cond и x: map(f,cond)(A.proj(x)) = B.proj(f(x)).

LaTeX

$$$$\\text{map}(f,\\mathrm{cond})(\\mathrm{A.proj}(x)) = \\mathrm{B.proj}(f(x)).$$$$

Lean4

@[simp]
theorem map_proj (cond : LEComap f A B) (x : X) : map f cond (A.proj x) = B.proj (f x) :=
  rfl

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

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

Разделы

Аффилиация

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