cylinder — Mathlib

English

A cylinder is the preimage of a base set S under the projection that forgets all coordinates not in a finite set s.

Русский

Цилиндр — это прообраз множества-основания S по проекции, которая забывает все координаты вне конечного множества s.

LaTeX

$$$$\\mathrm{cylinder}(s,S) = s_{\\text{restrict}}^{-1}'(S).$$$$

Lean4

/-- Given a finite set `s` of indices, a cylinder is the preimage of a set `S` of `∀ i : s, α i` by
the projection from `∀ i, α i` to `∀ i : s, α i`. -/
def cylinder (s : Finset ι) (S : Set (∀ i : s, α i)) : Set (∀ i, α i) :=
  s.restrict ⁻¹' S

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