image₂_inter_singleton — Mathlib

English

Let f: α → β → γ, b ∈ β, and s1, s2 ⊆ α. If f a is injective for a fixed a corresponding to b, then image₂ f (s1 ∩ s2) {b} = image₂ f s1 {b} ∩ image₂ f s2 {b}.

Русский

Пусть f: α → β → γ; для фиксированного a, если f a инъективна и b фиксирован, тогда image₂ f (s1 ∩ s2) {b} = image₂ f s1 {b} ∩ image₂ f s2 {b}.

LaTeX

$$$(Injective (f a)) \Rightarrow \mathrm{image}_2\ f\ (s_1 \cap s_2)\{b\} = \mathrm{image}_2\ f\ s_1\{b\} \cap \mathrm{image}_2\ f\ s_2\{b\}$$$

Lean4

theorem image₂_inter_singleton [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective fun a => f a b) :
    image₂ f (s₁ ∩ s₂) { b } = image₂ f s₁ { b } ∩ image₂ f s₂ { b } := by
  simp_rw [image₂_singleton_right, image_inter _ _ hf]

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