nonempty

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.IsCocircuit.nonempty

English

A cocircuit is nonempty.

Русский

Кококрит непустой.

LaTeX

$$$\text{IsCocircuit}_M(C) \Rightarrow C \neq \emptyset$$$

Lean4

theorem nonempty (hC : M.IsCocircuit C) : C.Nonempty :=
  hC.isCircuit.nonempty

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

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

Разделы

Аффилиация

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