mem_map — Mathlib

English

A point x lies in the image K.map f if and only if there exists y ∈ K with f y = x.

Русский

Элемент x принадлежит образу K.map f тогда, когда существует y ∈ K such that f y = x.

LaTeX

$$$$\forall {R} {L} {L_2} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L] (f : \text{LieHom } R L L_2) (K : \text{LieSubalgebra } R L) (x : L_2),\ x \in K.map f \iff \exists y : L, y \in K \wedge f y = x.$$$$

Lean4

@[simp]
theorem mem_map (x : L₂) : x ∈ K.map f ↔ ∃ y : L, y ∈ K ∧ f y = x :=
  Submodule.mem_map

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