inf_biInf — Mathlib

English

Interchanging infimum with biInf (dual of Sup) to obtain a symmetric equality.

Русский

Замена инфимума на биИнф даёт симметричное равенство.

LaTeX

$$$ \\inf_{i} \\big( \\bigwedge_{j \\in s} f(i,j) \\big) = \\bigwedge_{j \\in s} \\inf_{i} f(i,j). $$$

Lean4

theorem inf_biInf {p : ι → Prop} {f : ∀ i, p i → α} {a : α} (h : ∃ i, p i) :
    (a ⊓ ⨅ (i) (h : p i), f i h) = ⨅ (i) (h : p i), a ⊓ f i h :=
  @sup_biSup αᵒᵈ ι _ p f _ h

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