preimage_coe_self_inter — Mathlib

English

The preimage under inclusion of s ∩ t equals the preimage of t.

Русский

Предобраз включения от s ∩ t равен предобразу t.

LaTeX

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

Lean4

theorem preimage_coe_self_inter (s t : Set α) : ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t := by
  rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]
    -- Not `@[simp]` since `simp` can prove this.

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