mem_map_of_surjective — Mathlib

English

If f is surjective, then every y in I.map f can be written as f x for some x in I.

Русский

Если f сюръективен, то каждый элемент y ∈ I.map f имеет вид f x для некоторого x ∈ I.

LaTeX

$$$\forall y \in I.\mathrm{map}\ f\ y \,\exists x \in I : f(x) = y$$$

Lean4

theorem mem_map_of_surjective {y : L'} (h₁ : Function.Surjective f) (h₂ : y ∈ I.map f) : ∃ x : I, f x = y :=
  by
  rw [← LieSubmodule.mem_toSubmodule, coe_map_of_surjective h₁, Submodule.mem_map] at h₂
  obtain ⟨x, hx, rfl⟩ := h₂
  use ⟨x, hx⟩
  rw [LieHom.coe_toLinearMap]

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