ssubset_indep — Mathlib

English

If C is a circuit of M and X is a proper subset of C, then X is independent in M.

Русский

Если C — цикл M и X является корректно вложенным подмножеством C, то X независимо в M.

LaTeX

$$$M\IsCircuit(C)\wedge X\subset C\ \Rightarrow\ M.Indep(X)$$$

Lean4

theorem ssubset_indep (hC : M.IsCircuit C) (hXC : X ⊂ C) : M.Indep X :=
  by
  rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]
  exact fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

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