doubleXIso₁ — Mathlib

English

If φ and φ' are morphisms from K to double f hi, agreeing on i0 and i1 implies φ = φ'.

Русский

Если φ и φ' — морфизмы из K к double f hi и совпадают на i0 и i1, то φ = φ'.

LaTeX

$$$\forall (φ φ' : K \to \text{double } f hi₀₁),\; φ.f i₀ = φ'.f i₀ ∧ φ.f i₁ = φ'.f i₁ \Rightarrow φ = φ'$$$

Lean4

/-- The isomorphism `(double f hi₀₁).X i₁ ≅ X₁`. -/
noncomputable def doubleXIso₁ (h : i₀ ≠ i₁) : (double f hi₀₁).X i₁ ≅ X₁ :=
  eqToIso
    (by
      dsimp [double]
      rw [if_neg h.symm, if_pos rfl])

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