forall_subset_range_iff — Mathlib

English

For any f and p, (∀ s ⊆ range f, p s) ↔ ∀ s, p(f''s).

Русский

Для любой функции f и свойства p: (∀ s ⊆ range f, p(s)) эквивалентно (∀ s, p(f''s)).

LaTeX

$$$ (\\forall S, S \\subseteq \\mathrm{range}(f) \\Rightarrow p(S)) \\iff (\\forall S, p(\\mathrm{image}(f)(S))). $$$

Lean4

@[simp]
theorem forall_subset_range_iff {f : α → β} {p : Set β → Prop} : (∀ s, s ⊆ range f → p s) ↔ ∀ s, p (f '' s) := by
  rw [← forall_mem_range, range_image]; simp only [mem_powerset_iff]

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