preimage_val_eq_preimage_val_iff — Mathlib

English

Equality of preimages under Subtype.val is equivalent to equality of intersections with s.

Русский

Равенство предобразов Subtype.val эквивалентно равенству пересечений с s.

LaTeX

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

Lean4

theorem preimage_val_eq_preimage_val_iff (s t u : Set α) :
    (Subtype.val : s → α) ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u :=
  preimage_coe_eq_preimage_coe_iff

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