exists_set_subtype — Mathlib

English

There exists a subset s ⊆ t such that p((( inclusion )'' s)) holds, equivalently there exists s ⊆ α with p s.

Русский

Существует множество s ⊆ t, такое что p(((∈)'' s)) выполняется, эквивалентно существует s ⊆ α, такое что p s.

LaTeX

$$$ \exists s : Set t, p (((\uparrow) : t \to \alpha) '' s) \quad \text{iff}\quad \exists s : Set \alpha, s \subseteq t \land p s $$$

Lean4

theorem exists_set_subtype {t : Set α} (p : Set α → Prop) :
    (∃ s : Set t, p (((↑) : t → α) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s := by rw [← exists_subset_range_and_iff, range_coe]

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