preimage_union — Mathlib

English

The preimage of a union equals the union of preimages, under suitable injectivity hypotheses.

Русский

Предобраз объединения равно объединению предобразов при подходящих условиях инъективности.

LaTeX

$$$$ \\mathrm{preimage}(s \\cup t,f,hst) = \\mathrm{preimage}(s,f,\\cdot) \\cup \\mathrm{preimage}(t,f,\\cdot). $$$$

Lean4

@[simp]
theorem preimage_union [DecidableEq α] [DecidableEq β] {f : α → β} {s t : Finset β} (hst) :
    preimage (s ∪ t) f hst =
      (preimage s f fun _ hx₁ _ hx₂ => hst (mem_union_left _ hx₁) (mem_union_left _ hx₂)) ∪
        preimage t f fun _ hx₁ _ hx₂ => hst (mem_union_right _ hx₁) (mem_union_right _ hx₂) :=
  Finset.coe_injective (by simp)

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