le_inf_mul — Mathlib

English

For a semilattice inf and top, a ≤ inf(s * t) f is equivalent to a ≤ f(x*y) for all x ∈ s, y ∈ t.

Русский

Для полуупорядоченного отношения инф и верх, a ≤ inf(s * t) f эквивалентно a ≤ f(x*y) для всех x ∈ s, y ∈ t.

LaTeX

$$a \\le inf (s * t) f \\iff \\forall x \\in s, \\forall y \\in t, a \\le f (x * y)$$

Lean4

@[to_additive (attr := simp (default + 1))]
theorem le_inf_mul {β} [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
    a ≤ inf (s * t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y) :=
  le_inf_image₂

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