finset — Mathlib

English

Given a cylinder-tuple, there is a finite set of indices corresponding to it.

Русский

Дано цилиндрическое описание, существует конечное множество индексов, соответствующее ему.

LaTeX

$$$ \\mathrm{finset}(ht) : \\text{Finset of indices associated to } t \\in \\mathrm{measurableCylinders}(\\alpha) $$$

Lean4

/-- A finset `s` such that `t = cylinder s S`. `S` is given by `measurableCylinders.set`. -/
noncomputable def finset (ht : t ∈ measurableCylinders α) : Finset ι :=
  ((mem_measurableCylinders t).mp ht).choose

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