instCompleteLattice — Mathlib

English

The collection of intermediate fields forms a complete lattice under inclusion.

Русский

Множество промежуточных полей образует полную решётку по включению.

LaTeX

$$CompleteLattice (IntermediateField F E)$$

Lean4

instance : CompleteLattice (IntermediateField F E)
    where
  __ := GaloisInsertion.liftCompleteLattice IntermediateField.gi
  bot :=
    { toSubalgebra := ⊥
      inv_mem' := by rintro x ⟨r, rfl⟩; exact ⟨r⁻¹, map_inv₀ _ _⟩ }
  bot_le x := (bot_le : ⊥ ≤ x.toSubalgebra)

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