cylinder_eq_pi — Mathlib

English

The cylinder around x of length n is the finite product of singletons: cylinder x n = Set.pi (Finset.range n) (λ i, {x i}).

Русский

Цилиндр вокруг x длины n равен конечному произведению: cylinder x n = Set.pi (Finset.range n) (λ i, {x i}).

LaTeX

$$$\\mathrm{cylinder}(x,n)=\\mathrm{Set.pi}(\\mathrm{Finset.range}\\,n:\\mathrm{Set}\\mathbb{N})\\; (\\lambda i:\\mathbb{N}, \\{x(i)\\})$$$

Lean4

theorem cylinder_eq_pi (x : ∀ n, E n) (n : ℕ) : cylinder x n = Set.pi (Finset.range n : Set ℕ) fun i : ℕ => {x i} :=
  by
  ext y
  simp [cylinder]

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