other_ne — Mathlib

English

If z is not diagonal and a ∈ z, then the other element of z is not equal to a.

Русский

Если z не диагонален и a принадлежит z, то другой элемент z не равен a.

LaTeX

$$$$ (\neg \IsDiag(z)) \wedge (a \in z) \Rightarrow \text{the other element of } z \neq a. $$$$

Lean4

theorem other_ne {a : α} {z : Sym2 α} (hd : ¬IsDiag z) (h : a ∈ z) : Mem.other h ≠ a :=
  by
  contrapose! hd
  have h' := Sym2.other_spec h
  rw [hd] at h'
  rw [← h']
  simp

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