forall_set_subtype — Mathlib

English

All images of subsets of t under inclusion satisfy p iff all subsets s ⊆ t satisfy p.

Русский

Все образе подмножеств t через включение удовлетворяют p тогда и только тогда, когда все подмножества s ⊆ t удовлетворяют p.

LaTeX

$$$ \forall s : Set t, p ((\uparrow) : t \to \alpha) '' s \iff \forall s : Set \alpha, s \subseteq t \to p s $$$

Lean4

theorem forall_set_subtype {t : Set α} (p : Set α → Prop) :
    (∀ s : Set t, p (((↑) : t → α) '' s)) ↔ ∀ s : Set α, s ⊆ t → p s := by rw [← forall_subset_range_iff, range_coe]

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