eventually_isSelfAdjoint — Mathlib

English

Along the increasing approximate unit, eventually an element becomes self-adjoint.

Русский

Вдоль возрастающей аппроксимированной единицы элемент в конечном счёте становится самоприведенным.

LaTeX

$$$$ \text{Eventually } \text{IsSelfAdjoint } x $$$$

Lean4

theorem eventually_isSelfAdjoint {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : ∀ᶠ x in l, IsSelfAdjoint x :=
  hl.eventually_nonneg.mp <| .of_forall fun _ ↦ IsSelfAdjoint.of_nonneg

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