of_div_right — Mathlib

English

Dividing a set by a singleton {b} yields the set {(• / b) | x ∈ s}. In other words, s / {b} = { x / b : x ∈ s }.

Русский

Разделение множества на множество-одиночку {b} дает множество { x / b | x ∈ s }. Иными словами, s / {b} = { x / b : x ∈ s }.

LaTeX

$$$ s / \{ b \} = \{ x / b \mid x \in s \}$$$

Lean4

@[to_additive]
theorem of_div_right : (s / t).Nonempty → t.Nonempty :=
  Nonempty.of_image2_right

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