div_left — Mathlib

English

If T is a lower set in α, then S / T is an upper set for any S ⊆ α. Here S / T = { x ∈ α | ∃ s ∈ S, ∃ t ∈ T, s / t = x }.

Русский

Если T — нижнее множество в α, то S / T является верхним множеством (для любого S ⊆ α). Здесь S / T = { x ∈ α | ∃ s ∈ S, ∃ t ∈ T, s / t = x }.

LaTeX

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

Lean4

@[to_additive]
theorem div_left (ht : IsLowerSet t) : IsUpperSet (s / t) :=
  ht.toDual.div_left

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