instDiv — Mathlib

English

For any two upper sets S,T, the quotient S / T is the upper set { x y^{-1} | x ∈ S, y ∈ T }.

Русский

Для любых верхних множеств S и T отношение деления определяется как { x y^{-1} | x ∈ S, y ∈ T }, и остаётся верхним множеством.

LaTeX

$$$S,T \\in \\text{UpperSet}(\\alpha) \\implies S / T = \\{ x y^{-1} : x \\in S, y \\in T \\}$$$

Lean4

@[to_additive]
instance : Div (UpperSet α) :=
  ⟨fun s t ↦ ⟨image2 (· / ·) s t, s.2.div_right⟩⟩

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