domDomCongr_eq_iff — Mathlib

English

Two alternating maps are sent to the same by domDomCongr σ if and only if the maps are equal.

Русский

Две чередующихся карты переходят в одну и ту же через domDomCongr σ тогда и только тогда, когда сами карты равны.

LaTeX

$$$f.domDomCongr(σ) = g.domDomCongr(σ) \\;\\Leftrightarrow\\; f = g$$$

Lean4

/-- The results of applying `domDomCongr` to two maps are equal if and only if those maps are. -/
@[simp]
theorem domDomCongr_eq_iff (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) : f.domDomCongr σ = g.domDomCongr σ ↔ f = g :=
  (domDomCongrEquiv σ : _ ≃+ M [⋀^ι']→ₗ[R] N).apply_eq_iff_eq

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