def definition def or abbrev

`StructuredSet`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 155def StructuredSet : Set ℝ := {x : ℝ | 0 < x ∧ defect x = 0}

Definition body.

From the project-wide theorem graph. These declarations reference this one in their body.

complete_law_of_existence in IndisputableMonolith.Foundation.LawOfExistence decl_use
existence_economically_inevitable in IndisputableMonolith.Foundation.LawOfExistence decl_use
mem_structured_iff_exists in IndisputableMonolith.Foundation.LawOfExistence decl_use
structured_set_singleton in IndisputableMonolith.Foundation.LawOfExistence decl_use

Lean names referenced from this declaration's body.