filter_piFinset_of_notMem — Mathlib

English

If a finite index set ι is nonempty and s is nonempty, then the piFinset built from the constant family s is nonempty.

Русский

Если индексное множество ι непустое и s непусто, то piFinset, сконструированное из константного семейства s, непусто.

LaTeX

$$$\\forall \\beta, \\text{If } s \\text{ Nonempty, then } (\\operatorname{piFinset}(\\lambda _ : ι, s)).\\text{Nonempty}.$$$

Lean4

theorem filter_piFinset_of_notMem (t : ∀ a, Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) :
    {f ∈ piFinset t | f a = x} = ∅ := by simp only [filter_eq_empty_iff, mem_piFinset]; rintro f hf rfl; exact hx (hf _)

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