nontrivial_iff_exists_ne

Mathlib.Logic.Nontrivial.Defs

URI: https://scilib.ai/kg/mathlib#nontrivial_iff_exists_ne

English

For a fixed element x, Nontrivial α is equivalent to the existence of y ≠ x.

Русский

Для фиксированного элемента x: неtrivial α эквивально существованию y ≠ x.

LaTeX

$$$\text{Nontrivial}(\alpha) \iff \exists y:\, \alpha, y \neq x$$$

Lean4

theorem nontrivial_iff_exists_ne (x : α) : Nontrivial α ↔ ∃ y, y ≠ x :=
  ⟨fun h ↦ @exists_ne α h x, fun ⟨_, hy⟩ ↦ nontrivial_of_ne _ _ hy⟩

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

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

Разделы

Аффилиация

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