domain of function parameter can be genralized #1297

Closed

Labels

enhancement ✨

Milestone

opened

on Aug 22, 2024

analysis/theories/lebesgue_measure.v

Line 1843 in 8acde98

Lemma measurable_funX {R : realType} D (f : R -> R) n : measurable_fun D f ->

Metadata

Assignees

No one assigned

Labels

enhancement ✨

Type

No type

Projects

No projects

Milestone

1.4.0

Relationships

None yet

Development

No branches or pull requests