forall_true_iff' — Mathlib

English

If p(a) is always equivalent to True for all a, then ∀ a, p(a) is equivalent to True.

Русский

Если для всех a выполняется p(a) ⇔ True, то ∀ a, p(a) ⇔ True.

LaTeX

$$$$\\forall a, p(a) \\iff True $$ given $\\forall a, p(a) \\leftrightarrow True$.$$

Lean4

theorem forall_true_iff' (h : ∀ a, p a ↔ True) : (∀ a, p a) ↔ True :=
  iff_true_intro fun _ ↦
    of_iff_true
      (h _)
        -- This is not marked `@[simp]` because `implies_true : (α → True) = True` works

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