symm_bijective

Mathlib.MeasureTheory.MeasurableSpace.Embedding

URI: https://scilib.ai/kg/mathlib#MeasurableEquiv.symm_bijective

← MathLib Explorer

English

The inverse map on measurable equivalences is a bijection.

Русский

Обратная карта на measurable эквиваленты является биекцией.

LaTeX

$$$$ \text{Bijective}(\mathrm{MeasurableEquiv}.\mathrm{symm}) $$$$

Lean4

theorem symm_bijective : Function.Bijective (MeasurableEquiv.symm : (α ≃ᵐ β) → β ≃ᵐ α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru