completelyDistribLatticeMinimalAxioms

Lean4
/-- Note that subgraphs do not form a Boolean algebra, because of `verts`. -/
def completelyDistribLatticeMinimalAxioms : CompletelyDistribLattice.MinimalAxioms G.Subgraph :=
  { Subgraph.distribLattice with
    le := (· ≤ ·)
    sup := (· ⊔ ·)
    inf := (· ⊓ ·)
    top := ⊤
    bot := ⊥
    le_top := fun G' => ⟨Set.subset_univ _, fun _ _ => G'.adj_sub⟩
    bot_le := fun _ => ⟨Set.empty_subset _, fun _ _ => False.elim⟩
    sSup := sSup
    le_sSup := fun s G' hG' => ⟨by apply Set.subset_iUnion₂ G' hG', fun _ _ hab => ⟨G', hG', hab⟩⟩
    sSup_le := fun s G' hG' =>
      ⟨Set.iUnion₂_subset fun _ hH => (hG' _ hH).1,
        by
        rintro a b ⟨H, hH, hab⟩
        exact (hG' _ hH).2 hab⟩
    sInf := sInf
    sInf_le := fun _ G' hG' => ⟨Set.iInter₂_subset G' hG', fun _ _ hab => hab.1 hG'⟩
    le_sInf := fun _ G' hG' =>
      ⟨Set.subset_iInter₂ fun _ hH => (hG' _ hH).1, fun _ _ hab => ⟨fun _ hH => (hG' _ hH).2 hab, G'.adj_sub hab⟩⟩
    iInf_iSup_eq := fun f => Subgraph.ext (by simpa using iInf_iSup_eq) (by ext; simp [Classical.skolem]) }
Похожие утверждения