biInf_congr — Mathlib

English

Let p : ι → Prop. If for all i, p i implies f i = g i, then the infimum over i with p i of f i equals that over i with p i of g i.

Русский

Пусть p : ι → Prop. Если для каждого i верно p i → f i = g i, то infimum над i с условием p i для f i равен infimum над i с условием p i для g i.

LaTeX

$$$$ (\forall i, p i \to f i = g i) \Rightarrow \bigwedge_i \bigwedge_{(hi : p i)} f i hi = \bigwedge_i \bigwedge_{(hi : p i)} g i hi $$$$

Lean4

theorem biInf_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) : ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), g i :=
  biSup_congr (α := αᵒᵈ) h

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