eq_of_isCircuit_mem

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsLoop.eq_of_isCircuit_mem

← MathLib Explorer

English

If e is a loop, and C is a circuit containing e, then C = {e}.

Русский

Если e — петля, а C является Circuit, содержащим e, то C = {e}.

LaTeX

$$$ M.IsLoop e \land M.IsCircuit C \land e \in C \Rightarrow C=\{e\} $$$

Lean4

theorem eq_of_isCircuit_mem (he : M.IsLoop e) (hC : M.IsCircuit C) (h : e ∈ C) : C = { e } := by
  rw [he.isCircuit.eq_of_subset_isCircuit hC (singleton_subset_iff.mpr h)]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru