ext_iff'

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.ext_iff'

English

Equivalence of ext_iff' states the same as ext but with a slightly different formulation.

Русский

Эквивалентность ext_iff' совпадает с экстанцией по формулировке

LaTeX

$$$\mu_1 = \mu_2 \iff \forall s, \mu_1(s) = \mu_2(s)$$$

Lean4

theorem ext_iff' : μ₁ = μ₂ ↔ ∀ s, μ₁ s = μ₂ s :=
  ⟨by rintro rfl s; rfl, fun h ↦ Measure.ext (fun s _ ↦ h s)⟩

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

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

Разделы

Аффилиация

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