le_mul_iff

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.le_mul_iff

English

Let h ≤ f * g. Then for all s ∈ f and t ∈ g, the product s * t ∈ h.

Русский

Пусть h ≤ f * g. Тогда для всех s ∈ f и t ∈ g, выполняется s * t ∈ h.

LaTeX

$$$$ h \le f * g \iff \forall \{s\}, s \in f \to \forall \{t\}, t \in g \to s * t \in h. $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru