dep_iff_superset_isCircuit' — Mathlib

English

Dependence of X is equivalent to the existence of a circuit inside X and X ⊆ E, i.e., M.Dep X iff (∃ C ⊆ X, M.IsCircuit C) ∧ X ⊆ M.E.

Русский

Зависимость множества X эквивалентна существованию окружности внутри X и включению X в E, то есть M.Dep X ⇔ (∃ C ⊆ X, M.IsCircuit C) ∧ X ⊆ M.E.

LaTeX

$$$M.Dep X \\iff (\\exists C, C \\subseteq X \\land M.IsCircuit C) \\land X \\subseteq M.E$$$

Lean4

/-- A version of `Matroid.dep_iff_superset_isCircuit` that has the supportedness hypothesis
as part of the equivalence, rather than a hypothesis. -/
theorem dep_iff_superset_isCircuit' : M.Dep X ↔ (∃ C, C ⊆ X ∧ M.IsCircuit C) ∧ X ⊆ M.E :=
  ⟨fun h ↦ ⟨h.exists_isCircuit_subset, h.subset_ground⟩, fun ⟨⟨C, hCX, hC⟩, h⟩ ↦ hC.dep.superset hCX⟩

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