Skip to content

Squeeze lemmas lacks the order of arguments #1972

@IshiguroYoshihiro

Description

@IshiguroYoshihiro

In the statements squeeze_cvge and squeeze_fin,
order of arguments of functions (f, g, h)
differs from squeeze_cvgr.

Lemma squeeze_cvgr f h g : (\near a, f a <= g a <= h a) ->
forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l.

Lemma squeeze_fin f g h : (\near a, f a <= g a <= h a) ->
(\near a, f a \is a fin_num) -> (\near a, h a \is a fin_num) ->
(\near a, g a \is a fin_num).

Lemma squeeze_cvge f g h : (\near a, f a <= g a <= h a) ->
forall (l : \bar R), f @ a --> l -> h @ a --> l -> g @ a --> l.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions