mem_comap — Mathlib

English

Let f: E → F be a linear map and C be a pointed cone in F. Then x belongs to the comap of C along f if and only if f(x) lies in C; i.e., x ∈ C.comap f ⇔ f(x) ∈ C.

Русский

Пусть f: E → F — линейное отображение, C — направленный конус в F. Тогда x принадлежит прообразу конуса по f тогда и только тогда, когда f(x) принадлежит C; то есть x ∈ C.comap f ⇔ f(x) ∈ C.

LaTeX

$$$x \in C^{-1}(f) \;\iff\; f(x) \in C$$$

Lean4

@[simp]
theorem mem_comap {f : E →ₗ[R] F} {C : PointedCone R F} {x : E} : x ∈ C.comap f ↔ f x ∈ C :=
  Iff.rfl

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