inj — Mathlib

English

The operation ofSet is injective: equality of images implies equality of inputs.

Русский

Операция ofSet инъективна: равенство образов влечёт равенство исходных объектов.

LaTeX

$$$\\forall x\\, y:\\ZFSet,\\; \\operatorname{Class}.ofSet(x) = \\operatorname{Class}.ofSet(y) \\Rightarrow x = y$$$

Lean4

theorem inj {x y : ZFSet.{u}} (h : (x : Class.{u}) = y) : x = y :=
  ZFSet.ext fun z => by
    change (x : Class.{u}) z ↔ (y : Class.{u}) z
    rw [h]

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