coheytingAlgebra — Mathlib

English

Pull back a CoheytingAlgebra along an injection, preserving top, bottom, negation and sdiff. Domain inherits a CoheytingAlgebra.

Русский

Вытягивание по инъекции для коейтинговой алгебры сохраняет ⊤, ⊥, отрицание и разность; область определения наследует коейтинговую алгебру.

LaTeX

$$$\text{Function.Injective.coheytingAlgebra}(f,hf,map\_sup,map\_inf,map\_top,map\_bot,map\_hnot,map\_sdiff) : \text{CoheytingAlgebra } \alpha$$$

Lean4

/-- Pullback a `CoheytingAlgebra` along an injection. -/
protected abbrev coheytingAlgebra [Max α] [Min α] [Top α] [Bot α] [HNot α] [SDiff α] [CoheytingAlgebra β] (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_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    CoheytingAlgebra α :=
  { __ := hf.generalizedCoheytingAlgebra f map_sup map_inf map_bot map_sdiff
    __ := ‹Top α›
    __ := ‹HNot α›
    le_top := fun a => by
      change f _ ≤ _
      rw [map_top]
      exact le_top,
    top_sdiff := fun a => hf <| by rw [map_sdiff, map_hnot, map_top, top_sdiff'] }
    -- See note [reducible non-instances]

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