piFinset_empty — Mathlib

English

If the index type α is nonempty, then piFinset consisting of empty Finsets at every index is empty.

Русский

Если индекс-тип α непустой, то piFinset, где на каждом индексе стоит пустое множество, пуст.

LaTeX

$$$[\\text{Nonempty }\\alpha]\\quad \\operatorname{piFinset}(\\lambda a.\\varnothing) = \\varnothing.$$$

Lean4

@[simp]
theorem piFinset_empty [Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (δ i)) = ∅ := by simp

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