mem_map — Mathlib

English

Membership in the image under a linear map is characterized by the existence of a preimage in the domain cone.

Русский

Членство в образе под линейным отображением эквивалентно существованию предобраза в исходном конусе.

LaTeX

$$y ∈ C.map f ↔ ∃ x ∈ C, f x = y$$

Lean4

@[simp]
theorem mem_map {f : E →ₗ[R] F} {C : PointedCone R E} {y : F} : y ∈ C.map f ↔ ∃ x ∈ C, f x = y :=
  Iff.rfl

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