pi_empty — Mathlib

English

If a ∉ s, then the pi over insert a s decomposes as a biUnion of images of Pi.cons applied to elements of s.pi t.

Русский

Если a ∉ s, то pi(insert a s) t распадается на объединение через b∈t(a) образов Pi.cons s a b применённых к элементам s.pi t.

LaTeX

$$$ pi(insert a s) t = (t a).biUnion (\\lambda b, image (Pi.cons s a b) (pi s t)). $$$

Lean4

@[simp]
theorem pi_empty {t : ∀ a : α, Finset (β a)} : pi (∅ : Finset α) t = singleton (Pi.empty β) :=
  rfl

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