forall_mem_target — Mathlib

English

For every predicate p on β, p holds on all y in e.target iff p(e x) holds for all x in e.source.

Русский

Для каждого предиката p на β верно: p(y) для всякого y в target(e) эквивалентно p(e x) для всякого x в source(e).

LaTeX

$$(∀ y ∈ e.target, p y) ↔ (∀ x ∈ e.source, p (e x))$$

Lean4

theorem forall_mem_target {p : β → Prop} : (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (e x) := by
  rw [← image_source_eq_target, forall_mem_image]

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