generalizedHeytingAlgebra — Mathlib

English

The product of bi-Heyting algebras is itself a bi-Heyting algebra, defined componentwise with both Heyting and Coheyting structures.

Русский

Произведение би-ейтинговых алгебр само является биейтинговой алгеброй, определения в каждом компоненте соответствуют исходным структурам.

LaTeX

$$$\text{Prod.instBiheytingAlgebra} (\alpha,\beta) = \text{BiheytingAlgebra}(\alpha \times \beta)$, где операции заданы покомпонентно: $\text{himp}_{(a,b),(c,d)} = (a\to c, b\to d)$, $\text{sdiff}_{(a,b),(c,d)} = (a\setminus c, b\setminus d)$ и т.д.$$

Lean4

/-- Pullback a `GeneralizedHeytingAlgebra` along an injection. -/
protected abbrev generalizedHeytingAlgebra [Max α] [Min α] [Top α] [HImp α] [GeneralizedHeytingAlgebra β] (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_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : GeneralizedHeytingAlgebra α :=
  { __ := hf.lattice f map_sup map_inf
    __ := ‹Top α›
    __ := ‹HImp α›
    le_top := fun a => by
      change f _ ≤ _
      rw [map_top]
      exact le_top,
    le_himp_iff := fun a b c => by
      change f _ ≤ _ ↔ f _ ≤ _
      rw [map_himp, map_inf, le_himp_iff] }
    -- See note [reducible non-instances]

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