congr

Mathlib.MeasureTheory.MeasurableSpace.Defs

URI: https://scilib.ai/kg/mathlib#MeasurableSet.congr

English

If s is measurable and s = t, then t is measurable.

Русский

Если множество s измеримо и s равно t, то и t измеримо.

LaTeX

$$$\MeasurableSet(s) \to (s = t) \to \MeasurableSet(t)$$$

Lean4

theorem congr {s t : Set α} (hs : MeasurableSet s) (h : s = t) : MeasurableSet t := by rwa [← h]

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

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

Разделы

Аффилиация

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