index — Mathlib

English

If h is a FineSubfamilyOn f s, then h.index is a set indexing a disjoint covering of almost every s.

Русский

Если h — тонкое подподсемейство f на s, то h.index есть множество, индексирующее раздельное покрытие почти всей части s.

LaTeX

$$$\\text{index}(h) \\subseteq X\\times\\mathrm{Set}X \\quad\\text{и}\\quad h.index\\text{ индексирует раздельное покрытие почти всей }s.$$$

Lean4

/-- Given `h : v.FineSubfamilyOn f s`, then `h.index` is a set parametrizing a disjoint
covering of almost every `s`. -/
protected def index : Set (X × Set X) :=
  h.exists_disjoint_covering_ae.choose

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