exists

Mathlib.Order.Synonym

URI: https://scilib.ai/kg/mathlib#Lex.exists

English

For any p : Lex α → Prop, (∃ a, p a) is equivalent to ∃ a, p (toLex a).

Русский

Для любого p : Lex α → Prop, (∃ a, p a) эквивалентно ∃ a, p (toLex a).

LaTeX

$$$\exists a, p\,a \iff \exists a, p(\mathrm{toLex}\,a)$$$

Lean4

@[simp]
theorem «exists» {p : Lex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toLex a) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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