card_le_card_image₂_left — Mathlib

English

If a ∈ s and the map a ↦ f(a,·) is injective, then for any Finset t, #t ≤ #image₂ f s t.

Русский

Пусть a ∈ s и отображение a ↦ f(a,·) инъективно. Тогда для любого Finset t выполняется: |t| ≤ |image₂ f s t|.

LaTeX

$$$(a\in s) \land \text{Injective}(f\,a) \Rightarrow \#t \leq \#(\mathrm{image}_2\ f\ s\ t)$$$

Lean4

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

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