inj — Mathlib

English

There is a protective lemma asserting that PEquiv.inj holds: if an element b lies in the image of a₁ and a₂, then a₁=a₂.

Русский

Существует лемма, гласящая, что если некоторый элемент принадлежит изображения двух предобразов, то предобраза совпадают.

LaTeX

$$$$ \\forall {a_1 a_2}, \\ b \\in f a_1 \\land b \\in f a_2 \\Rightarrow a_1=a_2. $$$$

Lean4

protected theorem inj (f : α ≃. β) {a₁ a₂ : α} {b : β} (h₁ : b ∈ f a₁) (h₂ : b ∈ f a₂) : a₁ = a₂ := by
  rw [← mem_iff_mem] at *; cases h : f.symm b <;> simp_all

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