Proofgold Proposition

∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ PNoLt_pwise (PNo_downc x0) (PNo_upc x1)

type
prop

theory
HotG

name
PNoLt_pwise_downc_upc

proof
PUQ2Y..

Megalodon
PNoLt_pwise_downc_upc

proofgold address
TMSZ2..^{PNoLt_pwise_downc_upc}

creator
4903 Pr6Pc../ae3f1..

owner
4903 Pr6Pc../ae3f1..

term root
2b8e3..