r_eq_none

Mathlib.Algebra.Homology.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.r_eq_none

English

If no i satisfies e.f i = i', then e.r i' = none.

Русский

Если не существует i с e.f i = i', то e.r i' = none.

LaTeX

$$$(\\forall i, e.f i \\neq i') \\Rightarrow e.r i' = \\text{none}$$$

Lean4

theorem r_eq_none (i' : ι') (hi : ∀ i, e.f i ≠ i') : e.r i' = none :=
  dif_neg
    (by
      rintro ⟨i, hi'⟩
      exact hi i hi')

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

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

Разделы

Аффилиация

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