Assert a structure exists with a given value for one field

Stream: Is there code for X?

[Hunter Monroe]

Is there a best practice for asserting that a structure exists meeting its internal criteria if one field has a given value, for instance, define a function of x':R with return type Prop, if there is a point (x',y,z) in the StandardTwoSimplex (see below) as defined in Mathematics in Lean? My eventual goal is: define isPolyTimeFunction, which takes a function \alpha\r\beta and has a return type Prop, returning true if the nested structure Computability.TMComputable.TM2ComputableInPolyTime exists with numerous criteria (there is a TM, a polynomial, encodings for inputs/outputs, (nested) with a halting computation for each a:\alpha with the correct output within the poly bound). So this def would return Prop rather than present the structure: def PolyTimeFunction {α β: Type} {ea : FinEncoding α} {eb : FinEncoding β} (f : α → β) := @TM2ComputableInPolyTime α β ea eb f. Apologies that is not a mwe but that would be huge.

x : R
y : R
z : R
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
z_nonneg : 0 ≤ z
sum_eq : x + y + z = 1```

[Yaël Dillies]

Maybe

def hunterPred (x' : R) : Prop := ∃ s : StandardTwoSimplex, s.x = x'

or even

def hunterPred : R → Prop := (· ∈ Set.range StandardTwoSimplex.x)

[Mario Carneiro]

(Use triple backtick for multiline code blocks, see #backticks)

[Hunter Monroe]

Apologies I realized f is not a field. I want to add a def at the end of TMComputable, but instead of def isPolyTimeFunction {α β: Type} {ea : FinEncoding α} {eb : FinEncoding β} (f : α → β) :Prop := ∃tmp : @TM2ComputableInPolyTime α β ea eb f, True, how do I assert that the structure is nonempty with that f (has a polytime TM computing f)? The structure already asserts all of the needed criteria.

[Yaël Dillies]

Nonempty TheStructure?

[Mario Carneiro]

@Hunter Monroe the triple backticks before and after need to be on their own line, or the first line of text will be eaten and it won't be highlighted