indep_iff_forall_subset_not_isCircuit'

English

Independence of I is equivalent to: all its subsets do not form a circuit, and I lies in the ground set E.

Русский

Независимость множества I эквивалентна тому, что никакое подмножество I не образует окружность, и I ⊆ E.

LaTeX

$$$M.Indep I \\iff (\\forall C, C \\subseteq I \\to \\neg M.IsCircuit C) \\land I \\subseteq M.E$$$

Lean4

/-- A version of `Matroid.indep_iff_forall_subset_not_isCircuit` that has the supportedness
hypothesis as part of the equivalence, rather than a hypothesis. -/
theorem indep_iff_forall_subset_not_isCircuit' : M.Indep I ↔ (∀ C, C ⊆ I → ¬M.IsCircuit C) ∧ I ⊆ M.E :=
  by
  simp_rw [indep_iff_not_dep, dep_iff_superset_isCircuit']
  aesop

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