card_image₂_singleton_left — Mathlib

English

Let f: α → β → γ be a function of two arguments. If the map a ↦ f(a,·) is injective, then for every Finset t ⊆ β, the cardinality of the two-argument image over the singleton {a} equals the cardinality of t. In symbols: Injective (f a) ⇒ #(image₂ f {a} t) = #t.

Русский

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

LaTeX

$$$\operatorname{Injective}(f\,a) \Rightarrow \#(\mathrm{image}_2\,f\{a\} t) = \#t$$$

Lean4

theorem card_image₂_singleton_left (hf : Injective (f a)) : #(image₂ f { a } t) = #t := by
  rw [image₂_singleton_left, card_image_of_injective _ hf]

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