isCircuit_antichain — Mathlib

English

Circuits form an antichain with respect to inclusion: no circuit is a proper subset of another circuit.

Русский

Циклы образуют антицепь по включению: ни один цикл не является правильной подпоследовательностью другого цикла.

LaTeX

$$$\forall C,D,\ M.IsCircuit(C) \land M.IsCircuit(D) \land C\subset D \Rightarrow C=D$$$

Lean4

theorem isCircuit_antichain : IsAntichain (· ⊆ ·) (setOf M.IsCircuit) := fun _ hC _ hC' hne hss ↦
  hne <| (IsCircuit.minimal hC').eq_of_subset hC.dep hss

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