inf_mono — Mathlib

English

Let s1, s2 be finite sets with s1 ⊆ s2. Then the infimum over s2 of f is less than or equal to the infimum over s1 of f: s2.inf f ≤ s1.inf f.

Русский

Пусть s1, s2 — конечные множества с условием s1 ⊆ s2. Тогда инфимум над s2 от f не больше инфимума над s1 от f: s2.inf f ≤ s1.inf f.

LaTeX

$$$(s_1 \\subseteq s_2) \\implies s_2\\inf f \\le s_1\\inf f$$$

Lean4

@[gcongr]
theorem inf_mono (h : s₁ ⊆ s₂) : s₂.inf f ≤ s₁.inf f :=
  Finset.le_inf (fun _ hb => inf_le (h hb))

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