isCauSeq_neg — Mathlib

English

A CauSeq abv f has the same Cauchy property as its negation: IsCauSeq abv (-f) iff IsCauSeq abv f.

Русский

Последовательность Коши относительно abv сохраняется при взятии противоположной: IsCauSeq abv (-f) эквивалично IsCauSeq abv f.

LaTeX

$$$IsCauSeq abv (-f) \\leftrightarrow IsCauSeq abv f$$$

Lean4

@[simp]
theorem _root_.isCauSeq_neg : IsCauSeq abv (-f) ↔ IsCauSeq abv f := by
  simp only [IsCauSeq, Pi.neg_apply, ← neg_sub', abv_neg]

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