le_div_iff — Mathlib

English

For all filters f, g, h, h ≤ f / g if and only if for every s ∈ f and t ∈ g, s / t ∈ h.

Русский

Для всех фильтров f, g, h выполняется h ≤ f / g тогда и только тогда, когда для каждого s ∈ f и t ∈ g выполняется s / t ∈ h.

LaTeX

$$$h \\le f / g \\iff \\forall s (s \\in f) \\rightarrow \\forall t (t \\in g) \\rightarrow s / t \\in h.$$$

Lean4

@[to_additive (attr := simp)]
protected theorem le_div_iff : h ≤ f / g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s / t ∈ h :=
  le_map₂_iff

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