free_bot

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.free_bot

← MathLib Explorer

English

If A is nontrivial, then A.Free ⊥.

Русский

Если A неприводим, то A.Free ⊥.

LaTeX

$$A ≠ ⊥ → A.Free (⊥ : SimpleGraph β)$$

Lean4

theorem free_bot (h : A ≠ ⊥) : A.Free (⊥ : SimpleGraph β) :=
  by
  rw [← edgeSet_nonempty] at h
  intro ⟨f, hf⟩
  absurd f.map_mem_edgeSet h.choose_spec
  rw [edgeSet_bot]
  exact Set.notMem_empty (h.choose.map f)

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

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

Разделы

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

Аффилиация

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