Dependent products of real vector spaces

Content created by Louis Wasserman.

Created on 2026-04-26.
Last modified on 2026-04-26.

module linear-algebra.dependent-products-real-vector-spaces where
Imports 
open import foundation.universe-levels

open import linear-algebra.dependent-products-vector-spaces
open import linear-algebra.real-vector-spaces

open import real-numbers.field-of-real-numbers

Idea

Given a family of real vector spaces Vᵢ indexed by i : I, the dependent product Πᵢ Vᵢ is a real vector space.

Definition

Π-ℝ-Vector-Space :
  {l1 l2 l3 : Level} (I : UU l1) (V : I → ℝ-Vector-Space l2 l3) →
  ℝ-Vector-Space l2 (l1 ⊔ l3)
Π-ℝ-Vector-Space {l2 = l2} =
  Π-Vector-Space (heyting-field-ℝ l2)

Recent changes