leftDual_mem_rightFixedPoint — Mathlib

English

R.leftDual(J) ∈ R.rightFixedPoints.

Русский

R.leftDual(J) принадлежит R.rightFixedPoints.

LaTeX

$$$R.\mathrm{leftDual} J \in R.\mathrm{rightFixedPoints}.$$$

Lean4

/-- `leftDual` maps every element `J` to `rightFixedPoints`. -/
theorem leftDual_mem_rightFixedPoint (J : Set α) : R.leftDual J ∈ R.rightFixedPoints :=
  by
  apply le_antisymm
  · apply R.gc_leftDual_rightDual.monotone_l; exact R.gc_leftDual_rightDual.le_u_l J
  · exact R.gc_leftDual_rightDual.l_u_le (R.leftDual J)

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