image_val_inj — Mathlib

English

For all D,E ⊆ A, equality of their images in α implies equality of the sets: (↑D) = (↑E) ⇒ D = E.

Русский

Для множеств D,E ⊆ A равенство их образов в α подразумевает равенство самих множеств: (↑D) = (↑E) ⇒ D = E.

LaTeX

$$$ \uparrow D = \uparrow E \Rightarrow D = E $$$

Lean4

@[simp]
theorem image_val_inj : (D : Set α) = ↑E ↔ D = E :=
  Subtype.val_injective.image_injective.eq_iff

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