surjective — Mathlib

English

If E.map φ = F, then the restriction φ.restrict has a surjective image onto F.

Русский

Если E.map φ = F, то ограничение φ. restrict отображает на F сюръективно.

LaTeX

$$$ \\text{surjective}(\\phi.restrict (le_of_eq h)) $ when $E.map φ = F$$$

Lean4

theorem surjective (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty E] [Nonempty F]
    (h : E.map φ = F) : Function.Surjective (AffineMap.restrict φ (le_of_eq h)) :=
  by
  rintro ⟨x, hx : x ∈ F⟩
  rw [← h, AffineSubspace.mem_map] at hx
  obtain ⟨y, hy, rfl⟩ := hx
  exact ⟨⟨y, hy⟩, rfl⟩

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