forall

Mathlib.Order.Synonym

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

English

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

Русский

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

LaTeX

$$$\forall p:\, Lex\,\alpha \to \mathrm{Prop},\quad (\forall a, p\,a) \iff \forall a, p(\mathrm{toLex}\,a)$$$

Lean4

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

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

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

Разделы

Аффилиация

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