beattySeq'_symmDiff_beattySeq_pos

English

For real r,s with hrs, the symmetric difference of {beattySeq' r k | k > 0} and {beattySeq s k | k > 0} equals {n | 0 < n}.

Русский

При r,s с hrs симметрическая разность {beattySeq' r k | k > 0} и {beattySeq s k | k > 0} равна {n | 0 < n}.

LaTeX

$$$\\{beattySeq' r k \\;|\\; k>0\\} \\triangle \\{beattySeq s k \\;|\\; k>0\\} = \\{n \\mid 0 < n\\}$$$

Lean4

theorem beattySeq'_symmDiff_beattySeq_pos {r s : ℝ} (hrs : r.HolderConjugate s) :
    {beattySeq' r k | k > 0} ∆ {beattySeq s k | k > 0} = {n | 0 < n} := by
  rw [symmDiff_comm, beattySeq_symmDiff_beattySeq'_pos hrs.symm]

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