preimage_coe_eq_preimage_coe_iff — Mathlib

English

Two preimages under Subtype.val are equal iff their intersections with s are equal.

Русский

Два предобраза Subtype.val равны тогда, когда их пересечения с s равны.

LaTeX

$$$ ((\uparrow) : s \to \alpha)^{-1} t = ((\uparrow) : s \to \alpha)^{-1} u \iff s \cap t = s \cap u $$$

Lean4

theorem preimage_coe_eq_preimage_coe_iff {s t u : Set α} : ((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ s ∩ t = s ∩ u :=
  by rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]

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