Helper

extend_project_id

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_nd

Type Lemma

Proof Lines 20

Signature

Lemma extend_project_id (u : 'I_n.+1 -> msg) (target : msg) (v : {ffun 'I_n.+1 -> msg}) : u ord_max \is a GRing.unit -> v \in linear_fiber_nd u target -> extend_to_fiber u target (project_fiber v) = v.

Description

extend then project is identity for fiber elements

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats