iInf_exists — Mathlib

English

Let p be a predicate and f: Exists p → α. Then iInf over all x equals iInf over pairs (i,h) with x = ⟨i,h⟩.

Русский

Пусть p — предикат и f: Exists p → α. Тогда iInf по всем x равен iInf по парам (i,h) с x = ⟨i,h⟩.

LaTeX

$$$\\\\bigwedge_{x} f(x) = \\\\bigwedge_{i} \\\\bigwedge_{h} f(i,h)$$$

Lean4

@[simp]
theorem iInf_exists {p : ι → Prop} {f : Exists p → α} : ⨅ x, f x = ⨅ (i) (h), f ⟨i, h⟩ :=
  @iSup_exists αᵒᵈ _ _ _ _

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