le_total_ideal — Mathlib

English

The set { S | A ≤ S } is totally ordered under inclusion.

Русский

Множество { S | A ≤ S } образует полную линейную упорядоченность по включению.

LaTeX

$$IsTotal { S // A ≤ S } LE.le$$

Lean4

instance le_total_ideal : IsTotal { S // A ≤ S } LE.le := by
  classical
  let _ : IsTotal (PrimeSpectrum A) (· ≤ ·) := ⟨fun ⟨x, _⟩ ⟨y, _⟩ => LE.isTotal.total x y⟩
  exact ⟨(primeSpectrumOrderEquiv A).symm.toRelEmbedding.isTotal.total⟩

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