div — Mathlib

English

If S and T are finite subsets of a set α with a division operation, then the set of all quotients S / T = { x / y : x ∈ S, y ∈ T } is finite.

Русский

Если S и T — конечные подмножества множества α с операцией деления, то множество всех частных элементов S / T = { x / y : x ∈ S, y ∈ T } конечно.

LaTeX

$$$\\operatorname{Fin}(S) \\land \\operatorname{Fin}(T) \\Rightarrow \\operatorname{Fin}(S/T)$$$$

Lean4

@[to_additive]
theorem div : s.Finite → t.Finite → (s / t).Finite :=
  .image2 _

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