subset_coe_filter_of_subset_forall

English

If t is a subset of s and p holds for every element of t, then t is contained in the filtered set s.filter p. In other words, whenever t ⊆ s and ∀ x ∈ t, p x, we have t ⊆ s.filter p.

Русский

Если t ⊆ s и для каждого x ∈ t верно p x, то t содержится в s.filter p.

LaTeX

$$$(t \\subseteq s) \\land (\\forall x \\in t, p\\,x) \\Rightarrow t \\subseteq s.filter p$$$

Lean4

theorem subset_coe_filter_of_subset_forall (s : Finset α) {t : Set α} (h₁ : t ⊆ s) (h₂ : ∀ x ∈ t, p x) :
    t ⊆ s.filter p := fun x hx => (s.coe_filter p).symm ▸ ⟨h₁ hx, h₂ x hx⟩

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