Nuprl Lemma : m-interior_wf

[X,A:Type].  ∀[d:metric(X)]. (m-interior(X;d;A) ∈ Type) supposing strong-subtype(A;X)


Proof




Definitions occuring in Statement :  m-interior: m-interior(X;d;A) metric: metric(X) strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a m-interior: m-interior(X;d;A) prop:

Latex:
\mforall{}[X,A:Type].    \mforall{}[d:metric(X)].  (m-interior(X;d;A)  \mmember{}  Type)  supposing  strong-subtype(A;X)



Date html generated: 2020_05_20-AM-11_44_12
Last ObjectModification: 2019_11_07-AM-10_14_47

Theory : reals


Home Index