Nuprl Definition : has-interior-point
has-interior-point(k;c;a) == ∃x:ℕk ⟶ ℚ. (rat-point-in-cube(k;x;c) ∧ rat-point-in-cube-interior(k;x;a))
Definitions occuring in Statement :
rat-point-in-cube-interior: rat-point-in-cube-interior(k;x;a),
rat-point-in-cube: rat-point-in-cube(k;x;c),
rationals: ℚ,
int_seg: {i..j-},
exists: ∃x:A. B[x],
and: P ∧ Q,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
rationals: ℚ,
and: P ∧ Q,
rat-point-in-cube: rat-point-in-cube(k;x;c),
rat-point-in-cube-interior: rat-point-in-cube-interior(k;x;a)
FDL editor aliases :
has-interior-point
Latex:
has-interior-point(k;c;a) ==
\mexists{}x:\mBbbN{}k {}\mrightarrow{} \mBbbQ{}. (rat-point-in-cube(k;x;c) \mwedge{} rat-point-in-cube-interior(k;x;a))
Date html generated:
2020_05_20-AM-09_19_07
Last ObjectModification:
2019_11_02-PM-05_31_58
Theory : rationals
Home
Index