sigmaIsoHom_surj

Mathlib.Topology.FiberPartition

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Fiber.sigmaIsoHom_surj

English

The map sigmaIsoHom f is surjective onto S.

Русский

sigmaIsoHom_f сюръективно отображает во S.

LaTeX

$$$$\operatorname{Im}(\sigmaIsoHom_f)=S.$$$$

Lean4

theorem sigmaIsoHom_surj : Function.Surjective (sigmaIsoHom f) := fun _ ↦
  ⟨⟨⟨_, ⟨⟨_, Set.mem_range_self _⟩, rfl⟩⟩, ⟨_, rfl⟩⟩, rfl⟩

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

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

Разделы

Аффилиация

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