English
Let s and t be subsets of a type with a division operation. The pointwise division of sets is defined by s / t = { x / y : x ∈ s, y ∈ t }.
Русский
Пусть S и T — подмножества множества, на котором определено деление. Поэлементное деление множеств определяется как S / T = { x / y : x ∈ S, y ∈ T }.
LaTeX
$$$ s / t = \{ x / y \mid x \in s, y \in t \}$$$
Lean4
/-- The pointwise division of sets `s / t` is defined as `{x / y | x ∈ s, y ∈ t}` in locale
`Pointwise`. -/
@[to_additive /-- The pointwise subtraction of sets `s - t` is defined as `{x - y | x ∈ s, y ∈ t}` in locale
`Pointwise`. -/
]
protected def div : Div (Set α) :=
⟨image2 (· / ·)⟩
