eq_cylinder — Mathlib

English

For ht witnessing membership, t equals the cylinder formed from the finite set and the base set.

Русский

Для ht, фиксирующего принадлежность, t равен цилиндру, образованному по конечному набору индексов и базовому множеству.

LaTeX

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

Lean4

theorem eq_cylinder (ht : t ∈ closedCompactCylinders X) :
    t = cylinder (closedCompactCylinders.finset ht) (closedCompactCylinders.set ht) :=
  ((mem_closedCompactCylinders t).mp ht).choose_spec.choose_spec.2.2

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