exists_subset_image_finite_and — Mathlib

English

For a function f: α → β and a subset s ⊆ α, there exists a finite subset t ⊆ f''s with p t if and only if there exists a finite subset t ⊆ s with p(f''t).

Русский

Пусть f: α → β и s ⊆ α. Существует конечное подмножество t ⊆ f[ s ] такое, что p(t), тогда существует конечное подмножество t ⊆ s такое, что p(f''t).

LaTeX

$$$ (\\exists t \\subseteq f '' s, t.Finite \\land p t) \\iff (\\exists t \\subseteq s, t.Finite \\land p (f '' t)) $$$

Lean4

theorem exists_subset_image_finite_and {f : α → β} {s : Set α} {p : Set β → Prop} :
    (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t) := by
  classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _), Finset.subset_set_image_iff]
  aesop

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