forall_mem_map — Mathlib

English

An assertion about a property p holding for all elements y in s.map f is equivalent to the corresponding statement for all x in s, using the embedding.

Русский

Свойство p, которое истинно для всех элементов y в s.map f, эквивалентно соответствующему утверждению для всех x в s через вложение.

LaTeX

$$$ (\\forall y (H : y \\in s.map f), p\,y\,H) \\\\iff \\\\ (\\\\forall x (H : x \\in s), p (f x) (mem_map_of_mem _ H)) $$$

Lean4

theorem forall_mem_map {f : α ↪ β} {s : Finset α} {p : ∀ a, a ∈ s.map f → Prop} :
    (∀ y (H : y ∈ s.map f), p y H) ↔ ∀ x (H : x ∈ s), p (f x) (mem_map_of_mem _ H) := by grind

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