Widget for 3d Display of subsets of ℝ³

Stream: lean4

[Ron Z.]

Is there a widget for displaying subsets of ℝ³? I would like to be able to pan and rotate graphs of subsets of ℝ³ like the ones in my work.

rhinologic_figure_2.stl
rhinologic_figure_1.obj

Screenshot-2024-06-16-at-2.11.54AM.png

It would be great if there were a process for voxelizing .stl and .obj files into triple arrays.

[Yaël Dillies]

any subset of $ℝ^3$ is going to be challenging, since that includes the Cantor set, non-measurable sets, etc... Can you be more precise on what kind of sets you want to display?

[Kevin Buzzard]

I'm not sure what an .obj file of the Cantor set will look like... I think these things must use floats I guess? (I am not a computer scientist ;-) ) Floats are a finite field so Yael's objections are solved.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

https://github.com/bollu/polyscope.lean by @Siddharth Bhat might be of interest to you

[Siddharth Bhat]

@Ron Z. the polyscope code that @Wojciech Nawrocki posted can render .obj files, I'm pretty sure. It uses three.js to perform the rendering, and the code posted has Lean code that parses an obj file, and then ships it off to three.js for rendering.