mapNatBool — Mathlib

English

A map from a measurable space to the Cantor-like space ℕ → Bool is defined by membership in a countable generating sequence.

Русский

Отображение из измеримого пространства в пространство вида ℕ → Bool задается через членство в последовательности порождающих множеств.

LaTeX

$$$\\text{def } mapNatBool [MeasurableSpace α] [CountablyGenerated α] (x : α) (n : \\mathbb{N}) := x \\in natGeneratingSequence α n$$$

Lean4

/-- A map from a measurable space to the Cantor space `ℕ → Bool` induced by a countable
sequence of sets generating the measurable space. -/
noncomputable def mapNatBool [MeasurableSpace α] [CountablyGenerated α] (x : α) (n : ℕ) : Bool :=
  x ∈ natGeneratingSequence α n

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