eq_homEquiv_apply — Mathlib

English

Let A ∈ C, B ∈ D, f: F(A) → B and g: A → G(B). Then adj.homEquiv A B f = g if and only if (adj.homEquiv A B).symm g = f.

Русский

Пусть A ∈ C, B ∈ D, f: F(A) → B и g: A → G(B). Тогда adj.homEquiv A B f = g тогда и только если (adj.homEquiv A B).symm g = f.

LaTeX

$$$ adj.homEquiv A B f = g \iff (adj.homEquiv A B).symm g = f $$$

Lean4

theorem eq_homEquiv_apply {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    g = adj.homEquiv A B f ↔ (adj.homEquiv A B).symm g = f :=
  eq_unit_comp_map_iff adj f g

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