fundCircuit_isCircuit — Mathlib

English

If B is a base of M, x ∈ E, and x ∉ B, then the fundamental circuit of x with respect to B is a circuit.

Русский

Если B является базисом M, x ∈ E и x ∉ B, то фундаментальная окружность x относительно B является окружностью.

LaTeX

$$$\\forall {\\alpha} (M : Matroid \\alpha) {B : Set \\alpha}, M.IsBase B \\to x \\in M.E \\to x \\notin B \\to M.IsCircuit (M.fundCircuit x B)$$$

Lean4

theorem fundCircuit_isCircuit {B : Set α} (hB : M.IsBase B) (hxE : x ∈ M.E) (hxB : x ∉ B) :
    M.IsCircuit (M.fundCircuit x B) :=
  hB.indep.fundCircuit_isCircuit (by rwa [hB.closure_eq]) hxB

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