rightDual_mem_leftFixedPoint — Mathlib

English

R.rightDual(I) ∈ R.leftFixedPoints.

Русский

R.rightDual(I) принадлежит R.leftFixedPoints.

LaTeX

$$$R.\mathrm{rightDual} I \in R.\mathrm{leftFixedPoints}.$$$

Lean4

/-- `rightDual` maps every element `I` to `leftFixedPoints`. -/
theorem rightDual_mem_leftFixedPoint (I : Set β) : R.rightDual I ∈ R.leftFixedPoints :=
  by
  apply le_antisymm
  · apply R.gc_leftDual_rightDual.monotone_u; exact R.gc_leftDual_rightDual.l_u_le I
  · exact R.gc_leftDual_rightDual.le_u_l (R.rightDual I)

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