card_le_card_image₂_right — Mathlib

English

If b ∈ t and the map x ↦ f(x,b) is injective, then #s ≤ #image₂ f s t.

Русский

Если b ∈ t и отображение x ↦ f(x,b) инъективно, то для любого s выполняется: |s| ≤ |image₂ f s t|.

LaTeX

$$$\text{hb} : b \in t \quad \land \text{Injective}(\lambda x. f x b) \Rightarrow \#s \leq \#(\mathrm{image}_2\ f\ s\ t)$$$

Lean4

theorem card_le_card_image₂_right {t : Finset β} (hb : b ∈ t) (hf : Injective (f · b)) : #s ≤ #(image₂ f s t) :=
  card_le_card_of_injOn (f · b) (fun _ ha ↦ mem_image₂_of_mem ha hb) hf.injOn

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