is_sol_iff_mem_solSpace — Mathlib

English

A sequence u is a solution of E if and only if it belongs to the solution space E.solSpace.

Русский

Последовательность u является решением E тогда и только тогда, когда она принадлежит пространству решений E.solSpace.

LaTeX

$$$E.IsSolution\, u \;\iff\; u \in E.solSpace$$$

Lean4

/-- Defining property of the solution space : `u` is a solution
  iff it belongs to the solution space. -/
theorem is_sol_iff_mem_solSpace (u : ℕ → R) : E.IsSolution u ↔ u ∈ E.solSpace :=
  Iff.rfl

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