map_all_iff — Mathlib

English

For any f : α → β and p : β → Prop, (∀ x ∈ s.map f, p x) is equivalent to (∀ x ∈ s, p (f x)).

Русский

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

LaTeX

$$$(\forall x \in (s.map\ f),\ p\ x) \iff (\forall x \in s,\ p\ (f\ x))$$$

Lean4

theorem map_all_iff {β : Type u} {f : α → β} {p : β → Prop} {s : Seq α} :
    (∀ x ∈ (s.map f), p x) ↔ (∀ x ∈ s, (p ∘ f) x) :=
  by
  refine ⟨fun _ _ hx ↦ ?_, fun _ _ hx ↦ ?_⟩
  · solve_by_elim [mem_map f hx]
  · obtain ⟨_, _, hx'⟩ := exists_of_mem_map hx
    rw [← hx']
    solve_by_elim

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