injective_mapNatBool — Mathlib

English

If α is countably generated and separates points, then mapNatBool is injective.

Русский

Если α — счетно порожденное пространство и разделяет точки, то mapNatBool инъективен.

LaTeX

$$$Injective (mapNatBool α)$$$

Lean4

theorem injective_mapNatBool [MeasurableSpace α] [CountablyGenerated α] [SeparatesPoints α] :
    Injective (mapNatBool α) := by
  intro x y hxy
  rw [← generateFrom_natGeneratingSequence α] at *
  apply separating_of_generateFrom (range (natGeneratingSequence _))
  rintro - ⟨n, rfl⟩
  rw [← decide_eq_decide]
  exact congr_fun hxy n

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