mem_map — Mathlib

English

Membership in the mapped cone corresponds to membership in the closure of the mapped pointed cone.

Русский

Членство в образованном конусе соответствует членству в замкнутом образе направленного конуса.

LaTeX

$$y ∈ C.map f ↔ y ∈ (C.toPointedCone.map (f : E →ₗ[R] F)).closure$$

Lean4

@[simp]
theorem mem_map {f : E →L[R] F} {C : ProperCone R E} {y : F} :
    y ∈ C.map f ↔ y ∈ (C.toPointedCone.map (f : E →ₗ[R] F)).closure :=
  .rfl

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