dependent_iff_not_independent

Mathlib.LinearAlgebra.Projectivization.Independence

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

← MathLib Explorer

English

Dependence is equivalent to the negation of independence: Dependent f iff not Independent f.

Русский

Зависимость равносильна отрицанию независимости: Dependent f iff Not Independent f.

LaTeX

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

Lean4

/-- Dependence is the negation of independence. -/
theorem dependent_iff_not_independent : Dependent f ↔ ¬Independent f := by rw [dependent_iff, independent_iff]

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

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

Разделы

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

Аффилиация

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