cons_ne_zero_iff

Mathlib.Data.Finsupp.Fin

URI: https://scilib.ai/kg/mathlib#Finsupp.cons_ne_zero_iff

← MathLib Explorer

English

cons y s ≠ 0 iff y ≠ 0 or s ≠ 0.

Русский

cons y s ≠ 0 тогда и только тогда, когда y ≠ 0 или s ≠ 0.

LaTeX

$$$\\text{cons} y s \\neq 0 \\iff (y \\neq 0) \\lor (s \\neq 0)$$$

Lean4

theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 :=
  by
  refine ⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩
  refine imp_iff_not_or.1 fun h' c => h ?_
  rw [h', c, Finsupp.cons_zero_zero]

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

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

Разделы

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

Аффилиация

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