finset — Mathlib

English

A witness ht that t belongs to closedCompactCylinders X yields a finite index set ht and a corresponding S such that t = cylinder (ht) (S).

Русский

Для ht, свидетельствующего о принадлежности t к closedCompactCylinders X, существует конечный набор индексов ht и соответствующее S, что t = cylinder(ht,S).

LaTeX

$$$$t \\in \\text{closedCompactCylinders}(X) \\Rightarrow t = \\mathrm{cylinder}(\\text{closedCompactCylinders.finset}(\\mathrm{ht})) (\\mathrm{closedCompactCylinders.set}(\\mathrm{ht})).$$$$

Lean4

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

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