forall₃_true_iff — Mathlib

English

For any β: α → Sort*, γ: ∀ a, β a → Sort*, the statement ∀ a, ∀ b, γ(a,b) → True is equivalent to True.

Русский

Для любых β и γ: α → Sort*, ∀ a, β a → Sort* утверждение ∀ a ∀ b γ(a,b) → True эквивалентно True.

LaTeX

$$$$\\forall (a) (b : \\beta a), \\gamma(a,b) \\to True \\iff True.$$$$

Lean4

theorem forall₃_true_iff {β : α → Sort*} {γ : ∀ a, β a → Sort*} : (∀ (a) (b : β a), γ a b → True) ↔ True := by simp

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