set — Mathlib

English

The set closedCompactCylinders.set ht gives the base S for t, and t equals cylinder with s and S.

Русский

Множество closedCompactCylinders.set ht задаёт основание S для t, и t равен цилиндру с s и S.

LaTeX

$$$$t = \\mathrm{cylinder}(\\mathrm{closedCompactCylinders.finset}(\\mathrm{ht}), \\mathrm{closedCompactCylinders.set}(\\mathrm{ht})).$$$$

Lean4

/-- A set `S` such that `t = cylinder s S`. `s` is given by `closedCompactCylinders.finset`. -/
def set (ht : t ∈ closedCompactCylinders X) : Set (Π i : closedCompactCylinders.finset ht, X i) :=
  ((mem_closedCompactCylinders t).mp ht).choose_spec.choose

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