ne_or_ne

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Ne.ne_or_ne

English

For any α, x,y ∈ α and z ∈ α, if x ≠ y then x ≠ z ∨ y ≠ z.

Русский

Для любых x,y,z из α, если x ≠ y, то либо x ≠ z, либо y ≠ z.

LaTeX

$$$$\\forall {x,y,z:\\alpha}, x \\neq y \\to (x \\neq z \\lor y \\neq z).$$$$

Lean4

theorem ne_or_ne {x y : α} (z : α) (h : x ≠ y) : x ≠ z ∨ y ≠ z :=
  not_and_or.1 <| mt (and_imp.2 (· ▸ ·)) h.symm

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

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

Разделы

Аффилиация

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