inf_image — Mathlib

English

Infimum commutes with image under a function: the infimum of the image of s under f equals the infimum of g ∘ f over s when g is applied after f.

Русский

Infimum сохраняется при образе функции: (s.image f).inf g = s.inf (g ∘ f).

LaTeX

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

Lean4

@[simp]
theorem inf_image [DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α) : (s.image f).inf g = s.inf (g ∘ f) :=
  fold_image_idem

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