leftDual_rightDual_le_of_le — Mathlib

English

If I' is a right fixed point and I ≤ I', then leftDual(rightDual(I)) ≤ I'.

Русский

Если I' — правый фиксированный пункт и I ≤ I', тогда leftDual(rightDual(I)) ≤ I'.

LaTeX

$$$\forall I,I' \subseteq \beta,\ I' \in R.\mathrm{rightFixedPoints} \land I \subseteq I' \Rightarrow R.\mathrm{leftDual}(R.\mathrm{rightDual} I) \subseteq I'.)$$$

Lean4

theorem leftDual_rightDual_le_of_le {I I' : Set β} (h : I' ∈ R.rightFixedPoints) (h₁ : I ≤ I') :
    R.leftDual (R.rightDual I) ≤ I' := by
  rw [← h]
  apply R.gc_leftDual_rightDual.monotone_l
  apply R.gc_leftDual_rightDual.monotone_u
  exact h₁

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