exists_nat_measurableEquiv_range_coe_fin_of_finite

English

For a finite type α, there exists a measurable equivalence α ≃ᵐ range of a finite embedding into ℝ.

Русский

Для конечного типа α существует измеримое эквивалентство с образом под вложением в ℝ.

LaTeX

$$∃ n, Nonempty (α ≃ᵐ range (↑ : Fin n → ℝ))$$

Lean4

theorem exists_nat_measurableEquiv_range_coe_fin_of_finite [Finite α] :
    ∃ n : ℕ, Nonempty (α ≃ᵐ range ((↑) : Fin n → ℝ)) :=
  by
  obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α
  refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩
  exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)

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