div_right — Mathlib

English

If S is an upper set in a ordered commutative group α, then the right-division S / T is also an upper set for any T ⊆ α. Here S / T = { x ∈ α | ∃ s ∈ S, ∃ t ∈ T, s / t = x }.

Русский

Пусть S — верхнее множество в упорядоченной коммутативной группе α, тогда для любого T ⊆ α множество S / T также является верхним множеством. Здесь S / T = { x ∈ α | ∃ s ∈ S, ∃ t ∈ T, s / t = x }.

LaTeX

$$$\\text{IsUpperSet}(S) \\Rightarrow \\text{IsUpperSet}(S / T)$$$

Lean4

@[to_additive]
theorem div_right (hs : IsUpperSet s) : IsUpperSet (s / t) :=
  by
  rw [div_eq_mul_inv]
  exact hs.mul_right

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