map_top_of_surjective

Mathlib.MeasureTheory.OuterMeasure.Operations

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.map_top_of_surjective

English

If f is surjective, map f ⊤ = ⊤.

Русский

Если f сюръективна, то map f ⊤ = ⊤.

LaTeX

$$$ map\ f\ \top = \top $$$

Lean4

@[simp]
theorem map_top_of_surjective (f : α → β) (hf : Surjective f) : map f ⊤ = ⊤ := by
  rw [map_top, hf.range_eq, restrict_univ]

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

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

Разделы

Аффилиация

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