Naming for prop valued structure fields

Stream: mathlib4

[Arien Malec]

I wanted to highlight a review comment for mathlib4#698

Since Finite and Infinite are classes, I named the field value for notFinite according to the naming spec.

@Winston Yin noted:
"I understand the (WIP) naming convention says that structure fields should be lowerCamelCase, but Prop-valued fields are often exported as theorems, which should be lower_snake_case. Mathport defaults to not_finite here. Perhaps worth discussing on Zulip."

[Winston Yin]

I started a convo here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Prop.60-valued.20field.20names/near/311933755