image_inter_of_injOn — Mathlib

English

If f is injective on s ∪ t, then the image of (s ∩ t) under f equals the intersection of the images: (s ∩ t).image f = s.image f ∩ t.image f.

Русский

Если f инъективна на объединении s и t, то образ пересечения равен пересечению образов: (s ∩ t).image f = s.image f ∩ t.image f.

LaTeX

$$$(\,s \cap t\,).image f = s.image f \cap t.image f$ (при условии, что hf : \text{Set.InjOn } f (s \cup t))$$$

Lean4

theorem image_inter_of_injOn [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Set.InjOn f (s ∪ t)) :
    (s ∩ t).image f = s.image f ∩ t.image f :=
  coe_injective <| by
    push_cast
    exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

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