le_inf_div — Mathlib

English

Let α be a type, β a Semilattice with Inf and Top, s,t Finset α, f: α → β, a ∈ β. Then a ≤ inf (s / t) f holds iff for all x ∈ s and y ∈ t, a ≤ f(x/y).

Русский

Пусть α — множество, β — полугруппа с Inf и Top, s,t — конечные множества, f: α → β, a ∈ β. Тогда a ≤ inf (s/t) f эквивалентно тому, что для всех x ∈ s и y ∈ t выполняется a ≤ f(x/y).

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_div [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
    a ≤ inf (s / t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y) :=
  le_inf_image₂

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