map_finset_inf' — Mathlib

English

If f is a homomorphism that preserves infimum, then applying f to the infimum over a finite set equals the infimum of the mapped values; i.e., f( inf' f-set ) = inf' (f ∘ values).

Русский

Если f сохраняет инфимума, то применение f к инфимума над конечным множеством равно инфимууму от образа под f.

LaTeX

$$$f( \\inf'_{H} g ) = \\inf'_{H} (f \\circ g)$$$

Lean4

@[simp]
theorem _root_.map_finset_inf' [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) {s : Finset ι} (hs)
    (g : ι → α) : f (s.inf' hs g) = s.inf' hs (f ∘ g) := by refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]

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