map_finset_inf — Mathlib

English

For a function f and a Finset s with an inf-preserving property, f( s.inf g ) = s.inf ( f ∘ g ).

Русский

Для функции f и Finset s с сохранением инфимума выполняется f( s.inf g ) = s.inf ( f ∘ g ).

LaTeX

$$$ f (s.inf g) = s.inf (g \circ f) $$$

Lean4

@[simp]
theorem _root_.map_finset_inf [SemilatticeInf β] [OrderTop β] [FunLike F α β] [InfTopHomClass F α β] (f : F)
    (s : Finset ι) (g : ι → α) : f (s.inf g) = s.inf (f ∘ g) :=
  Finset.cons_induction_on s (map_top f) fun i s _ h => by rw [inf_cons, inf_cons, map_inf, h, Function.comp_apply]

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