eq_iff — Mathlib

English

For a function f of two arguments that is Injective2, the equality f a1 b1 = f a2 b2 holds exactly when a1 = a2 and b1 = b2.

Русский

Для функции f: α → β → γ, удовлетворяющей Injective2, равенство f a1 b1 = f a2 b2 происходит тогда и только тогда, когда a1 = a2 и b1 = b2.

LaTeX

$$$ \forall {\alpha} {\beta} {\gamma} {f : \alpha \to \beta \to \gamma},\; \operatorname{Injective2} f \Rightarrow \forall {a1 a2} {b1 b2}, f a1 b1 = f a2 b2 \leftrightarrow a1 = a2 \wedge b1 = b2$$$

Lean4

theorem eq_iff (hf : Injective2 f) {a₁ a₂ b₁ b₂} : f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ :=
  ⟨fun h ↦ hf h, fun ⟨h1, h2⟩ ↦ congr_arg₂ f h1 h2⟩

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