Let X, Tx, g and h be given.
Assume Hgcont: continuous_map X Tx R R_standard_topology g.
Assume Hhcont: continuous_map X Tx R R_standard_topology h.
We will prove closed_in X Tx {x ∈ X|Rle (apply_fun g x) (apply_fun h x)}.
Set B to be the term {x ∈ X|Rlt (apply_fun h x) (apply_fun g x)}.
We prove the intermediate claim HBopen: B ∈ Tx.
An exact proof term for the current goal is (continuous_Rlt_preimage_open_swapped X Tx g h Hgcont Hhcont).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (continuous_map_topology_dom X Tx R R_standard_topology g Hgcont).
We prove the intermediate claim Heq: {x ∈ X|Rle (apply_fun g x) (apply_fun h x)} = X ∖ B.
Apply set_ext to the current goal.
Let x be given.
Assume HxA: x ∈ {x0 ∈ X|Rle (apply_fun g x0) (apply_fun h x0)}.
We will prove x ∈ X ∖ B.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ Rle (apply_fun g x0) (apply_fun h x0)) x HxA).
We prove the intermediate claim Hle: Rle (apply_fun g x) (apply_fun h x).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ Rle (apply_fun g x0) (apply_fun h x0)) x HxA).
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun h x) (apply_fun g x)).
An exact proof term for the current goal is (RleE_nlt (apply_fun g x) (apply_fun h x) Hle).
We prove the intermediate claim HxNotB: x ∉ B.
Assume HxB: x ∈ B.
We will prove False.
We prove the intermediate claim Hlt: Rlt (apply_fun h x) (apply_fun g x).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ Rlt (apply_fun h x0) (apply_fun g x0)) x HxB).
An exact proof term for the current goal is (Hnlt Hlt).
An exact proof term for the current goal is (setminusI X B x HxX HxNotB).
Let x be given.
Assume HxXB: x ∈ X ∖ B.
We will prove x ∈ {x0 ∈ X|Rle (apply_fun g x0) (apply_fun h x0)}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X B x HxXB).
We prove the intermediate claim HxNotB: x ∉ B.
An exact proof term for the current goal is (setminusE2 X B x HxXB).
We prove the intermediate claim Hgfun: function_on g X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology g Hgcont).
We prove the intermediate claim Hhfun: function_on h X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology h Hhcont).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (Hgfun x HxX).
We prove the intermediate claim HhxR: apply_fun h x ∈ R.
An exact proof term for the current goal is (Hhfun x HxX).
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun h x) (apply_fun g x)).
Assume Hlt: Rlt (apply_fun h x) (apply_fun g x).
We will prove False.
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ Rlt (apply_fun h x0) (apply_fun g x0)) x HxX Hlt).
An exact proof term for the current goal is (HxNotB HxB).
We prove the intermediate claim Hle: Rle (apply_fun g x) (apply_fun h x).
An exact proof term for the current goal is (RleI (apply_fun g x) (apply_fun h x) HgxR HhxR Hnlt).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ Rle (apply_fun g x0) (apply_fun h x0)) x HxX Hle).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (closed_of_open_complement X Tx B HTx HBopen).
∎