Dependent — Mathlib

English

Independent f is equivalent to not being dependent; that is, independence is the negation of dependence.

Русский

Независимость f эквивалентна не зависимому; независимость есть отрицание зависимости.

LaTeX

$$$Independent(f) \\iff \\lnot Dependent(f)$$$

Lean4

/-- A linearly dependent family of nonzero vectors gives a dependent family of points
in projective space. -/
inductive Dependent : (ι → ℙ K V) → Prop
  | mk (f : ι → V) (hf : ∀ i : ι, f i ≠ 0) (h : ¬LinearIndependent K f) : Dependent fun i => mk K (f i) (hf i)

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