ext

Mathlib.MeasureTheory.MeasurableSpace.Embedding

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

English

Two measurable equivalences are equal if their underlying functions coincide.

Русский

Две измеримые эквивалентности равны, если их опорные функции совпадают.

LaTeX

$$$$ \\forall e_1,e_2:\\ α \\simeq^m β,\\; (e_1 : α \\to β) = e_2 \\Rightarrow e_1 = e_2. $$$$

Lean4

@[ext]
theorem ext {e₁ e₂ : α ≃ᵐ β} (h : (e₁ : α → β) = e₂) : e₁ = e₂ :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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