forall

Mathlib.Data.SetLike.Basic

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

English

For all x, q x holds iff for all x ∈ p, q ⟨x, h⟩ holds.

Русский

Для всех x справедливо q x тогда и только тогда, когда для всех x ∈ p верно q ⟨x, h⟩.

LaTeX

$$∀ x, q x ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, h⟩$$

Lean4

protected theorem «forall» {q : p → Prop} : (∀ x, q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩ :=
  SetCoe.forall

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

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

Разделы

Аффилиация

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