Nuprl Rule : orLevelFunctionality

H x:(P ∨ Q ∈ 𝕌{lvl}), J ⊢ A ∨ B ∈ 𝕌{lvl} ext experimental{orLevelFunctionality}(Ax)

  BY orLevelFunctionality #$i v ()
  
  H v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}

Latex:
H  x:(P  \mvee{}  Q  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  A  \mvee{}  B  \mmember{}  \mBbbU{}\{lvl\}  ext  experimental\{orLevelFunctionality\}(Ax)

    BY  orLevelFunctionality  \#\$i  v  ()
   
    H  v:(P  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  A  \mmember{}  \mBbbU{}\{lvl\}
    H  v:(Q  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  B  \mmember{}  \mBbbU{}\{lvl\}


Date html generated: 2019_06_20-PM-04_11_54
Last ObjectModification: 2016_01_12-PM-01_16_33

Theory : rules


Home Index