instFrame — Mathlib

English

If each π(i) is a frame, then the Pi-type ∀i, π(i) is a frame, with coordinate-wise structure.

Русский

Если каждый π(i) — рамка, то тип Pi, состоящий из функций i ↦ π(i), образует рамку с координатной структурой.

LaTeX

$$$\text{If } \{\pi(i)\}_{i} \text{ are frames, then } \prod_{i} \pi(i) \text{ is a frame.}$$$

Lean4

instance instFrame {ι : Type*} {π : ι → Type*} [∀ i, Frame (π i)] : Frame (∀ i, π i)
    where
  __ := instCompleteLattice
  __ := instHeytingAlgebra

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