map_mk — Mathlib

English

The map commutes with representatives mk, sending mk x to mk of the mapped x.

Русский

Картирует представителя mk так, что mk x переходит в mk отображенного x.

LaTeX

$$$$ \mathrm{map}(g)(\mathrm{mk} x) = \mathrm{mk}( g(x) ). $$$$

Lean4

theorem map_mk (g : A →+* B) (comap_le : P ≤ Q.comap g) (hg : ∀ i, ∀ a ∈ 𝒜 i, g a ∈ ℬ i) (x) :
    map 𝒜 ℬ g comap_le hg (mk x) = mk ⟨x.1, ⟨_, hg _ _ x.2.2⟩, ⟨_, hg _ _ x.3.2⟩, comap_le x.4⟩ :=
  rfl

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