mul_subset_iff — Mathlib

English

For Finsets s, t, u ⊆ α, the product s * t is contained in u if and only if every product x*y with x ∈ s and y ∈ t lies in u.

Русский

Для конечных множеств s, t, u ⊆ α, произведение s * t содержится в u тогда и только тогда для любых x ∈ s, y ∈ t произведение x*y ∈ u.

LaTeX

$$$s * t \\subseteq u \\quad\\text{iff}\\quad \\forall x \\in s, \\forall y \\in t,\\; x*y \\in u$$$

Lean4

@[to_additive]
theorem mul_subset_iff : s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u :=
  image₂_subset_iff

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