mk_eq_mk — Mathlib

English

Let p be a predicate on α. The map sending (a, h) with a ∈ α and h : p a to ⟨a, h⟩ is injective; equivalently, if ⟨a, h⟩ = ⟨a′, h′⟩ then a = a′.

Русский

Пусть p на α. Отображение, отправляющее пару (a, h) с a ∈ α и h : p a в ⟨a, h⟩, инъективно; то есть если ⟨a, h⟩ = ⟨a′, h′⟩, то a = a′.

LaTeX

$$$\forall a,a'\,\forall h: p(a), h': p(a'):\; @mk\alpha\, p\, a\, h = @mk\alpha\, p\, a'\, h' \Longleftrightarrow a = a' $$$

Lean4

/-- Restatement of `Subtype.mk.injEq` as an iff. -/
theorem mk_eq_mk {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' := by simp

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