restrict_dep_iff

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.restrict_dep_iff

English

The restricted dependent sets are exactly those X with ¬Indep(X) and X ⊆ R.

Русский

Зафиксированные зависимые множества равны тем X, для которых ¬Indep(X) и X ⊆ R.

LaTeX

$$(M ↾ R).Dep X ↔ (¬ M.Indep X ∧ X ⊆ R)$$

Lean4

@[simp]
theorem restrict_dep_iff : (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R := by rw [Dep, restrict_indep_iff, restrict_ground_eq];
  tauto

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

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

Разделы

Аффилиация

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