forall_congr_left

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.forall_congr_left

English

Let e: α ≃ β. Then (∀ a, p(a)) ↔ (∀ b, p(e.symm b)).

Русский

Пусть e: α ≃ β. Тогда (∀ a, p(a)) эквивалентно ∀ b, p(e.symm b).

LaTeX

$$$$ (\forall a, p(a)) \leftrightarrow (\forall b, p(e.symm(b))). $$$$

Lean4

protected theorem forall_congr_left : (∀ a, p a) ↔ ∀ b, p (e.symm b) :=
  e.symm.forall_congr_right.symm

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

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

Разделы

Аффилиация

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