div — Mathlib

English

The pointwise division s / t is the set of all quotients x / y with x ∈ s and y ∈ t.

Русский

По точечному делению Finset: 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 finsets `s / t` is defined as `{x / y | x ∈ s, y ∈ t}` in locale
`Pointwise`. -/
@[to_additive /-- The pointwise subtraction of finsets `s - t` is defined as `{x - y | x ∈ s, y ∈ t}`
      in scope `Pointwise`. -/
    ]
protected def div : Div (Finset α) :=
  ⟨image₂ (· / ·)⟩

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