all_iff_forall

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.all_iff_forall

← MathLib Explorer

English

For any P, All P t is equivalent to ∀ x, Emem x t → P x.

Русский

Для любого P, All P t эквивалентно ∀ x, Emem x t → P x.

LaTeX

$$All P t \iff \forall x, Emem x t \rightarrow P x$$

Lean4

theorem all_iff_forall {P : α → Prop} : ∀ {t}, All P t ↔ ∀ x, Emem x t → P x
  | nil => (iff_true_intro <| by rintro _ ⟨⟩).symm
  | node _ l x r => by simp [All, Emem, all_iff_forall, Any, or_imp, forall_and]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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