Nuprl Rule : imageEqInduction

H y:(t2 = (f t1) ∈ Image(A,f)) ⊢ t2 = (f t1) ∈ T

  BY imageEqInduction #$i a b z ()

  H  ⊢ f ∈ Base
  H  ⊢ t1 ∈ A
  H  ⊢ f t1 ∈ T
  H a:Base, b:Base, y:(f a ∈ T), z:(a = b ∈ A) ⊢ (f a) = (f b) ∈ T

Definitions occuring in rule : image-type: Image(T,f), base: Base, member: t ∈ T, equal: s = t ∈ T, apply: f a, axiom: Ax

Latex:
H y:(t2 = (f t1)) \mvdash{} t2 = (f t1) BY imageEqInduction \#\$i a b z () H \mvdash{} f \mmember{} Base H \mvdash{} t1 \mmember{} A H \mvdash{} f t1 \mmember{} T H a:Base, b:Base, y:(f a \mmember{} T), z:(a = b) \mvdash{} (f a) = (f b) Date html generated: 2019_06_20-PM-04_12_17 Last ObjectModification: 2019_01_02-PM-03_11_02 Theory : rules Home Index