forall_mem_map_iff — Mathlib

English

For any f : α → β, p : β → Prop, and s : Multiset α, we have (∀ y ∈ map f s, p y) ↔ ∀ x ∈ s, p (f x).

Русский

Для всех отображений f: α→β и свойств p на β: ∀ y ∈ map f s, p y эквивалентно ∀ x ∈ s, p (f x).

LaTeX

$$$$ (\\\\forall y \\,\\\\in \\,\\\\mathrm{map} f\, s, \\, p\, y) \\\\iff \\\\forall x \\,\\\\in \\, s, \\, p(map f x) $$$$

Lean4

theorem forall_mem_map_iff {f : α → β} {p : β → Prop} {s : Multiset α} : (∀ y ∈ s.map f, p y) ↔ ∀ x ∈ s, p (f x) :=
  Quotient.inductionOn' s fun _L => List.forall_mem_map

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