map_comp_proj

Mathlib.Topology.DiscreteQuotient

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

English

The map composed with A.proj equals the projection B.proj after applying cond.

Русский

Состав map с A.proj совпадает с проекцией B.proj после применения cond.

LaTeX

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

Lean4

@[simp]
theorem map_comp_proj (cond : LEComap f A B) : map f cond ∘ A.proj = B.proj ∘ f :=
  rfl

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

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

Разделы

Аффилиация

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