completelyDistribLattice — Mathlib

English

Pull back a CompletelyDistribLattice along an injection; α becomes a CompletelyDistribLattice under the induced structure.

Русский

Тянем назад CompletelyDistribLattice вдоль инъекции; α приобретает полностью распределимую структуру.

LaTeX

$$$[CompletelyDistribLattice\; \beta] \rightarrow \text{pullback along } f:\alpha \to \beta \Rightarrow CompletelyDistribLattice(\alpha).$$$

Lean4

/-- Pullback a `CompletelyDistribLattice` along an injection. -/
protected abbrev completelyDistribLattice [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α]
    [HNot α] [SDiff α] [CompletelyDistribLattice β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
    (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
    (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : CompletelyDistribLattice α
    where
  __ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
  __ := hf.biheytingAlgebra f map_sup map_inf map_top map_bot map_compl map_hnot map_himp map_sdiff
  iInf_iSup_eq
    g :=
    hf <| by
      simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range, iInf_iSup_eq]
        -- See note [reducible non-instances]

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