independent_iff_not_dependent

Mathlib.LinearAlgebra.Projectivization.Independence

URI: https://scilib.ai/kg/mathlib#Projectivization.independent_iff_not_dependent

← MathLib Explorer

English

Independence is equivalent to the negation of dependence.

Русский

Независимость равносильна отрицанию зависимости.

LaTeX

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

Lean4

/-- Independence is the negation of dependence. -/
theorem independent_iff_not_dependent : Independent f ↔ ¬Dependent f := by
  rw [dependent_iff_not_independent, Classical.not_not]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru