eq_of_sigmaMk_comp — Mathlib

English

If a ∘ f = b ∘ g for some γ ≠ ∅, then a = b and f ≍ g (HEq).

Русский

Если a ∘ f = b ∘ g, то a = b и f HEq g.

LaTeX

$$$ \text{If } \mathrm{Function.} \mathrm{comp}(\Sigma\text{mk } a) f = \mathrm{Function.} \mathrm{comp}(\Sigma\text{mk } b) g \;\Rightarrow\; a = b \land f \;HEq\; g $$$

Lean4

/-- A version of `Iff.mp Sigma.ext_iff` for functions from a nonempty type to a sigma type. -/
theorem _root_.Function.eq_of_sigmaMk_comp {γ : Type*} [Nonempty γ] {a b : α} {f : γ → β a} {g : γ → β b}
    (h : Sigma.mk a ∘ f = Sigma.mk b ∘ g) : a = b ∧ f ≍ g :=
  by
  rcases ‹Nonempty γ› with ⟨i⟩
  obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)
  simpa [funext_iff] using h

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