Helper

extend_in_fiber

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_nd

Type Lemma

Proof Lines 8

Signature

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

Description

extend_to_fiber produces a fiber element

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