isCircuit_restrict_of_subset — Mathlib

English

If C is a circuit and C ⊆ R, then the restriction M|R has C as a circuit.

Русский

Если C — цикл и C ⊆ R, то ограничение M|R имеет C в качестве цикла.

LaTeX

$$$M.IsCircuit(C) \land C \subseteq R \Rightarrow (M\restriction R).IsCircuit C$$$

Lean4

theorem isCircuit_restrict_of_subset (hC : M.IsCircuit C) (hCR : C ⊆ R) : (M ↾ R).IsCircuit C :=
  by
  simp_rw [isCircuit_iff, restrict_dep_iff, dep_iff, and_imp] at *
  exact ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩

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