tfae_of_forall

Mathlib.Data.List.TFAE

URI: https://scilib.ai/kg/mathlib#List.tfae_of_forall

English

If for every a the list l.map (p ↦ p a) has TFAE, then l.map (p ↦ ∀ a, p a) has TFAE.

Русский

Если для каждого a список l.map(p ↦ p a) имеет TFAE, то l.map(p ↦ ∀ a, p a) имеет TFAE.

LaTeX

$$$ (l.map (\p -> \forall a, p a)).TFAE $$$

Lean4

theorem tfae_of_forall (b : Prop) (l : List Prop) (h : ∀ a ∈ l, a ↔ b) : TFAE l := fun _a₁ h₁ _a₂ h₂ =>
  (h _ h₁).trans (h _ h₂).symm

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

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

Разделы

Аффилиация

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