Generalize to `l : \bar R`? #1485

Open

Labels

Milestone

opened

on Feb 18, 2025

analysis/theories/ftc.v

Line 900 in f29e974

Lemma le0_continuous_FTC2y (f F : R -> R) a (l : R) :

@IshiguroYoshihiro

Metadata

Assignees

No one assigned

Labels

Type

No type

Fields

No fields configured for issues without a type.

Projects

No projects

Milestone

1.17.0

Relationships

None yet

Development

No branches or pull requests