eq_cylinder — Mathlib

English

For ht in measurable cylinders, t equals the cylinder built from ht's finset and ht's base set.

Русский

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

LaTeX

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

Lean4

theorem eq_cylinder (ht : t ∈ measurableCylinders α) :
    t = cylinder (measurableCylinders.finset ht) (measurableCylinders.set ht) :=
  ((mem_measurableCylinders t).mp ht).choose_spec.choose_spec.right

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