proj_surjOn_baseSet — Mathlib

English

The projection maps e.source onto e.baseSet surjectively.

Русский

Проекция отображает e.source на e.baseSet сюръективно.

LaTeX

$$$\operatorname{SurjOn}(\mathrm{proj}, e.source, e.baseSet)$$$

Lean4

theorem proj_surjOn_baseSet [Nonempty F] : Set.SurjOn proj e.source e.baseSet := fun b hb =>
  let ⟨y⟩ := ‹Nonempty F›
  ⟨e.toPartialEquiv.symm (b, y), e.toPartialEquiv.map_target <| e.mem_target.2 hb, e.proj_symm_apply' hb⟩

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