compl_apply

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

URI: https://scilib.ai/kg/mathlib#Matrix.compl_apply

English

Each entry of A.compl is either 0 or 1.

Русский

Каждый элемент A.compl равен либо 0, либо 1.

LaTeX

$$$(A^{\\mathrm{compl}})_{ij} = 0 \\lor (A^{\\mathrm{compl}})_{ij} = 1$$$

Lean4

@[simp]
theorem compl_apply [Zero α] [One α] (i j : V) : A.compl i j = 0 ∨ A.compl i j = 1 :=
  by
  unfold compl
  split_ifs <;> simp

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

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

Разделы

Аффилиация

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