instCompleteLattice — Mathlib

Lean4
/-- The complete lattice structure on pretopologies. This is induced by the `InfSet` instance, but
with good definitional equalities for `⊥`, `⊤` and `⊓`. -/
instance : CompleteLattice (Pretopology C) where
  __ := orderBot C
  __ := orderTop C
  inf t₁
    t₂ :=
    { coverings := fun X ↦ t₁.coverings X ∩ t₂.coverings X
      has_isos := fun _ _ f _ ↦ ⟨t₁.has_isos f, t₂.has_isos f⟩
      pullbacks := fun _ _ f S hS ↦ ⟨t₁.pullbacks f S hS.left, t₂.pullbacks f S hS.right⟩
      transitive := fun _ S Ti hS hTi ↦
        ⟨t₁.transitive S Ti hS.left (fun _ f H ↦ (hTi f H).left),
          t₂.transitive S Ti hS.right (fun _ f H ↦ (hTi f H).right)⟩ }
  inf_le_left _ _ _ _ hS := hS.left
  inf_le_right _ _ _ _ hS := hS.right
  le_inf _ _ _ hts htr X _ hS := ⟨hts X hS, htr X hS⟩
  __ := completeLatticeOfInf _ (isGLB_sInf C)
Похожие утверждения