card_image₂_singleton_right — Mathlib

English

Let f: α → β → γ and a fixed b ∈ β. If the map a ↦ f(a,b) is injective, then for every Finset s ⊆ α, #(image₂ f s {b}) = #s.

Русский

Пусть f: α → β → γ и фиксированное b ∈ β. Если отображение a ↦ f(a,b) инъективно, то для любого конечного множества s ⊆ α выполняется #(image₂ f s {b}) = #s.

LaTeX

$$$(Injective\ (\lambda a. f\ a\ b)) \Rightarrow \#(\mathrm{image}_2\ f\ s\{b\}) = \#s$$$

Lean4

theorem card_image₂_singleton_right (hf : Injective fun a => f a b) : #(image₂ f s { b }) = #s := by
  rw [image₂_singleton_right, card_image_of_injective _ hf]

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