image_preimage_coe — Mathlib

English

The image under Subtype.val of the preimage under Subtype.val of t equals s ∩ t.

Русский

Образ Subtype.val от предобраза Subtype.val t равен s ∩ t.

LaTeX

$$$ \operatorname{image}(\operatorname{Subtype.val}, \operatorname{preimage}(\operatorname{Subtype.val}, t)) = s \cap t $$$

Lean4

@[simp]
theorem image_preimage_coe (s t : Set α) : ((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = s ∩ t :=
  image_preimage_eq_range_inter.trans <| congr_arg (· ∩ t) range_coe

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