not_isDiag_mk_of_mem_offDiag

Mathlib.Data.Finset.Sym

URI: https://scilib.ai/kg/mathlib#Finset.not_isDiag_mk_of_mem_offDiag

← MathLib Explorer

English

If a ∈ s.offDiag, then (Sym2.mk a) is not diagonal.

Русский

Если a ∈ s.offDiag, то (Sym2.mk a) не является диагональю.

LaTeX

$$a \in s.offDiag \Rightarrow \neg (Sym2.mk a).IsDiag$$

Lean4

theorem not_isDiag_mk_of_mem_offDiag {a : α × α} (h : a ∈ s.offDiag) : ¬(Sym2.mk a).IsDiag :=
  by
  rw [Sym2.isDiag_iff_proj_eq]
  exact (mem_offDiag.1 h).2.2

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

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

Разделы

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

Аффилиация

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