rightFixedPoints — Mathlib

English

RightFixedPoints is the set of I ⊆ β such that R.leftDual(R.rightDual(I)) = I.

Русский

RightFixedPoints — множество I ⊆ β, удовлетворяющих R.leftDual(R.rightDual(I)) = I.

LaTeX

$$$\mathrm{rightFixedPoints} = \{ I \subseteq \beta \mid R.\mathrm{leftDual}(R.\mathrm{rightDual} I) = I \}.$$$

Lean4

/-- `rightFixedPoints` is the set of elements `I : Set β` satisfying `leftDual (rightDual I) = I`.
-/
def rightFixedPoints :=
  {I : Set β | R.leftDual (R.rightDual I) = I}

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