diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1b864bc1d..0e70c8f6c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,186 @@ ### Added +- in `functions.v`: + + mixin ... + +- in `tvs.v`: + + ... +- in `derive.v`: + + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr` + + lemmas `derivable0`, `derive0`, `is_derive0` +- in `topology_structure.v`: + + lemma `not_limit_pointE` + +- in `separation_axioms.v`: + + lemmas `limit_point_closed` +- in `convex.v`: + + lemma `convex_setW` +- in `convex.v`: + + lemma `convexW` + ### Changed +- moved from `topology_structure.v` to `filter.v`: + + lemma `continuous_comp` (and generalized) + +- in set_interval.v + + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized) + +- in `set_interval.v` + + `itv_is_closed_unbounded` (fix the definition) + +- in `set_interval.v` + + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool) + +- in `lebesgue_Rintegrable.v`: + + lemma `Rintegral_cst` (does not use `cst` anymore) + +- split `probability.v` into directory `probability_theory` and move contents as: + + file `probability.v`: + + file `bernoulli_distribution.v`: + * definitions `bernoulli_pmf`, `bernoulli_prob` + * lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf`, + `eq_bernoulli`, `bernoulli_dirac`, `eq_bernoulliV2`, `bernoulli_probE`, + `measurable_bernoulli_prob`, `measurable_bernoulli_prob2` + + file `beta_distribution.v`: + * lemmas `continuous_onemXn`, `onemXn_derivable`, `derivable_oo_LRcontinuous_onemXnMr`, + `derive_onemXn`, `Rintegral_onemXn` + * definition `XMonemX` + * lemmas `XMonemX_ge0`, `XMonemX_le1`, `XMonemX0n`, `XMonemXn0`, `XMonemX00`, + `XMonemXC`, XMonemXM`, `continuous_XMonemX`, `within_continuous_XMonemX`, + `measurable_XMonemX`, `bounded_XMonemX`, `integrable_XMonemX`, `integrable_XMonemX_restrict`, + `integral_XMonemX_restrict` + * definition `beta_fun` + * lemmas `EFin_beta_fun`, `beta_fun_sym`, `beta_fun0n`, `beta_fun00`, `beta_fun1Sn`, + `beta_fun11`, `beta_funSSnSm`, `beta_funSnSm`, `beta_fun_fact`, `beta_funE`, + `beta_fun_gt0`, `beta_fun_ge0` + * definition `beta_pdf` + * lemmas `measurable_beta_pdf`, `beta_pdf_ge0`, `beta_pdf_le_beta_funV`, `integrable_beta_pdf`, + `bounded_beta_pdf_01` + * definition `beta_prob` + * lemmas integral_beta_pdf`, `beta_prob01`, `beta_prob_fin_num`, `beta_prob_dom`, + `beta_prob_uniform`, `integral_beta_prob_bernoulli_prob_lty`, + `integral_beta_prob_bernoulli_prob_onemX_lty`, + `integral_beta_prob_bernoulli_prob_onem_lty`, `beta_prob_integrable`, + `beta_prob_integrable_onem`, `beta_prob_integrable_dirac`, + `beta_prob_integrable_onem_dirac`, `integral_beta_prob` + * definition `div_beta_fun` + * lemmas `div_beta_fun_ge0`, `div_beta_fun_le1` + * definition `beta_prob_bernoulli_prob` + * lemmas `beta_prob_bernoulli_probE` + + file `binomial_distribution.v`: + * definition `binomial_pmf` + * lemmas `measurable_binomial_pmf` + * definition `binomial_prob` + * definition `bin_prob` + * lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, + `integral_binomial`, `integral_binomial_prob`, `measurable_binomial_prob` + + file `exponential_distribution.v`: + * definition `exponential_pdf` + * lemmas `exponential_pdf_ge0`, `lt0_exponential_pdf`, `measurable_exponential_pdf`, + `exponential_pdfE`, `in_continuous_exponential_pdf`, `within_continuous_exponential_pdf` + * definition `exponential_prob` + * lemmas `derive1_exponential_pdf`, `exponential_prob_itv0c`, `integral_exponential_pdf`, + `integrable_exponential_pdf` + + file `normal_distribution.v`: + * definition `normal_fun` + * lemmas `measurable_normal_fun`, normal_fun_ge0`, `normal_fun_center` + * definition `normal_peak` + * lemmas `normal_peak_ge0`, `normal_peak_gt0` + * definition `normal_pdf` + * lemmas `normal_pdfE`, `measurable_normal_pdf`, `normal_pdf_ge0`, `continuous_normal_pdf`, + `normal_pdf_ub` + * definition `normal_prob` + * lemmas `integral_normal_pdf`, `integrable_normal_pdf`, `normal_prob_dominates` + + file `poisson_distribution.v`: + * definition `poisson_pmf` + * lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf` + * definition `poisson_prob` + * lemma `measurable_poisson_prob` + + file `uniform_distribution.v`: + * definition `uniform_pdf` + * lemmas `uniform_pdf_ge0`, `measurable_uniform_pdf`, `integral_uniform_pdf`, + `integral_uniform_pdf1` + * definition `uniform_prob` + * lemmmas `integrable_uniform_pdf`, `dominates_uniform_prob`, + `integral_uniform` + + file `random_variable.v`: + * definition `random_variable` + * lemmas `notin_range_measure`, `probability_range` + * definition `distribution` + * lemmas `probability_distribution`, `ge0_integral_distribution`, `integral_distribution` + * definition `cdf` + * lemmas `cdf_ge0`, `cdf_le1`, `cdf_nondecreasing`, `cvg_cdfy1`, `cvg_cdfNy0`, + `cdf_right_continuous`, `cdf_lebesgue_stieltjes_id`, `lebesgue_stieltjes_cdf_id`, + * definition `ccdf` + * lemmas `cdf_ccdf_1` + * corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf` + * lemmas `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous` + * definition `expectation` + * lemmas `expectation_def`, `expectation_fin_num`, `expectation_cst`, + `expectation_indic`, `integrable_expectation`, `expectationZl`, + `expectation_ge0`, `expectation_le`, `expectationD`, `expectationB`, + `expectation_sum`, `ge0_expectation_ccdf` + * definition `covariance` + * lemmas `covarianceE`, `covarianceC`, `covariance_fin_num`, + `covariance_cst_l`, `covariance_cst_r`, `covarianceZl`, `covarianceZr`, + `covarianceNl`, `covarianceNr`, `covarianceNN`, `covarianceDl`, `covarianceDr`, + `covarianceBl`, `covarianceBr` + * definition `variance` + * lemmas `varianceE`, `variance_fin_num`, `variance_ge0`, `variance_cst`, + `varianceZ`, `varianceN`, `varianceD`, `varianceB`, `varianceD_cst_l`, `varianceD_cst_r`, + `varianceB_cst_l`, `varianceB_cst_r`, `covariance_le` + * definition `mmt_gen_fun` + * lemmas `markov`, `chernoff`, `chebyshev`, `cantelli` + * definition `discrete_random_variable` + * lemmas `dRV_dom_enum` + * definitions `dRV_dom`, `dRV_enum`, `enum_prob` + * lemmas `distribution_dRV_enum`, `distribution_dRV`, `sum_enum_prob` + * definition `pmf` + * lemmas `pmf_ge0`, `pmf_gt0_countable`, `pmf_measurable`, `dRV_expectation`, + `expectation_pmf` + +- moved from `convex.v` to `realfun.v` + + lemma `second_derivative_convex` + +- in classical_sets.v + + lemma `in_set1` (statement changed) + +- in `subspace_topology.v`: + + lemmas `open_subspaceP` and `closed_subspaceP` (use `exists2` instead of `exists`) +- moved from `filter.v` to `classical_sets.v`: + + definition `set_system` +- moved from `measurable_structure.v` to `classical_sets.v`: + + definitions `setI_closed`, `setU_closed` + +- moved from `theories` to `theories/topology_theory`: + + file `function_spaces.v` + +- moved from `theories` to `theories/normedtype_theory`: + + file `tvs.v` + +- moved from `tvs.v` to `pseudometric_normed_Zmodule.v`: + + definitions `NbhsNmodule`, `NbhsZmodule`, `PreTopologicalNmodule`, `PreTopologicalZmodule`, + `PreUniformNmodule`, `PreUniformZmodule` + +- in `tvs.v`, turned into `Let`'s: + + local lemmas `standard_add_continuous`, `standard_scale_continuous`, `standard_locally_convex` + +- in `normed_module.v`, turned into `Let`'s: + + local lemmas `add_continuous`, `scale_continuous`, `locally_convex` + +- moved from `normed_module.v` to `pseudometric_normed_Zmodule.v` and + generalized from `normedModType` to `pseudoMetricNormedZmodType` + + lemma `ball_open` (`0 < r` hypothesis also not needed anymore) + + lemma `near_shift` + + lemma `cvg_comp_shift` + + lemma `ball_open_nbhs` + +- moved from `tvs.v` to `convex.v` + + definition `convex`, renamed to `convex_set` + + definition `convex` + ### Renamed - in `tvs.v`: diff --git a/_CoqProject b/_CoqProject index 8b90d4861..182e2ecd8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -87,6 +87,8 @@ theories/normedtype_theory/urysohn.v theories/normedtype_theory/vitali_lemma.v theories/normedtype_theory/normedtype.v +theories/hahn_banach_theorem.v + theories/sequences.v theories/realfun.v theories/exp.v diff --git a/classical/filter.v b/classical/filter.v index 0cd56cf06..33096e489 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -946,6 +946,11 @@ Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) := (f%function @ x --> f%function x). Notation continuous f := (forall x, continuous_at x f). +Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x : + {for x, continuous f} -> {for (f x), continuous g} -> + {for x, continuous (g \o f)}. +Proof. exact: cvg_comp. Qed. + Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) : {for x, continuous f} -> (\forall y \near f x, P y) -> (\near x, P (f x)). diff --git a/classical/functions.v b/classical/functions.v index 77be38a0a..c68e035f8 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -128,6 +128,12 @@ Add Search Blacklist "_mixin_". (* fctE == multi-rule for fct *) (* ``` *) (* *) +(* ``` *) +(*Section linfun_lmodtype == canonical lmodtype structure on linear maps *) +(* between lmodtypes. *) +(* *) +(* *) +(* *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) @@ -2750,3 +2756,93 @@ End function_space_lemmas. Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f. Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed. + +Local Open Scope ring_scope. +Import GRing.Theory. + +Section linfun_pred. +Context {K : numDomainType} {E : lmodType K} {F : lmodType K} + {s : K -> F -> F}. + +(**md Beware that `lfun` is reserved for vector types, hence this one has been + named `linfun` *) +Definition linfun : {pred E -> F} := mem [set f | linear_for s f ]. +Definition linfun_key : pred_key linfun. Proof. exact. Qed. +Canonical linfun_keyed := KeyedPred linfun_key. + +End linfun_pred. + +Section linfun. +Context {R : numDomainType} {E : lmodType R} + {F : lmodType R} {s : GRing.Scale.law R F}. +Notation T := {linear E -> F | s}. +Notation linfun := (@linfun _ E F s). + +Section Sub. +Context (f : E -> F) (fP : f \in linfun). + +Definition linfun_Sub_subproof := + @GRing.isLinear.Build _ E F s f (set_mem fP). + +#[local] HB.instance Definition _ := linfun_Sub_subproof. +Definition linfun_Sub : {linear _ -> _ | _ } := f. +End Sub. + +Lemma linfun_rect (K : T -> Type) : + (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u. +Proof. +move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]]. +set G := (G in K G). +have Pf : f \in linfun by rewrite inE /= => // x u y; rewrite Pf2 Pf3. +suff -> : G = linfun_Sub Pf by apply: Ksub. +rewrite {}/G. +congr (GRing.Linear.Pack (GRing.Linear.Class _ _)). +- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance. +- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance. +Qed. + +Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP. + +Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of {linear E -> F | s} by <:]. + +Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type := + | Islinfun (l : {linear E -> F | s}) : linfun_spec f l true. + +Lemma linfunP (f : E -> F) : f \in linfun -> linfun_spec f f (f \in linfun). +Proof. +move=> /[dup] f_lc ->. +have {2}-> : f = linfun_Sub f_lc by rewrite linfun_valP. +by constructor. +Qed. + +End linfun. + +Section linfun_lmodtype. +Context {R : numFieldType} {E F : lmodType R}. + +Import GRing.Theory. + +Lemma linfun_submod_closed : submod_closed (@linfun R E F *:%R). +Proof. +split; first by rewrite inE; exact/linearP. +move=> r /= _ _ /linfunP[f] /linfunP[g]. +by rewrite inE /=; exact: linearP. +Qed. + +HB.instance Definition _ := + @GRing.isSubmodClosed.Build _ _ linfun linfun_submod_closed. + +HB.instance Definition _ := + [SubChoice_isSubLmodule of {linear E -> F } by <:]. + +End linfun_lmodtype. + +(* TODO: we wanted to declare this instance in classical_sets.v but failed and did not understand why, also we couldn't generaliz *) +HB.instance Definition _ {R : numDomainType} (E F : lmodType R) := + isPointed.Build {linear E -> F} (\0)%R. diff --git a/theories/Make b/theories/Make index 75ab71c74..cc3ad18fd 100644 --- a/theories/Make +++ b/theories/Make @@ -53,6 +53,8 @@ normedtype_theory/urysohn.v normedtype_theory/vitali_lemma.v normedtype_theory/normedtype.v +hahn_banach_theorem.v + realfun.v sequences.v exp.v diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v new file mode 100644 index 000000000..ad256f421 --- /dev/null +++ b/theories/hahn_banach_theorem.v @@ -0,0 +1,440 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import interval_inference. +From mathcomp Require Import unstable wochoice boolp classical_sets topology reals. +From mathcomp Require Import filter reals normedtype convex. +Import numFieldNormedType.Exports. +Local Open Scope classical_set_scope. + +(* Marie's proposal: encode the "partial" properties by reasoning on + the graph of functions. The other option would be to study a partial + order defined on subsets of the ambiant space V, on which it is possible + to obtain a bounded lineEar form extending f. But this options seems much + less convenient, in particular when establishing that one can extend f + on a space with one more dimension. Indeed, exhibiting a term of type + V -> R requires a case ternary analysis on F, the new line, and an + explicit direct sum to ensure the definition is exhaustive. Working with + graphs allows to leave this argument completely implicit. *) + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + + + + +Local Open Scope ring_scope. +Local Open Scope convex_scope. +Local Open Scope real_scope. +Import GRing.Theory. +Import Num.Theory. + + +Module Lingraph. +Section Lingraphsec. + +Variables (R : numDomainType) (V : lmodType R). + +Definition graph := V -> R -> Prop. + +Definition linear_graph (f : graph) := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + +Variable f : graph. +Hypothesis lrf : linear_graph f. + +Lemma lingraph_00 x r : f x r -> f 0 0. + Proof. + suff -> : f 0 0 = f (x + (-1) *: x) (r + (-1) * r) by move=> h; apply: lrf. + by rewrite scaleNr mulNr mul1r scale1r !subrr. + Qed. + + Lemma lingraph_scale x r l : f x r -> f (l *: x) (l * r). + Proof. + move=> fxr. + have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r. + by apply: lrf=> //; apply: lingraph_00 fxr. + Qed. + + Lemma lingraph_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2). + Proof. + have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r. + have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r. + by apply: lrf. + Qed. + + + Definition add_line f w a := fun v r => + exists v' : V, exists r' : R, exists lambda : R, + [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. + +End Lingraphsec. +End Lingraph. + + +Section HBPreparation. +Import Lingraph. + (* TODO: getting rid of relations and linear relations to make Zorn act on functions only ? *) + +Variables (R : realType) (V : lmodType R) (F : pred V). + +Variables (F' : subLmodType F) (phi : {linear F' -> R}) (p : V -> R). + +Implicit Types (f g : graph V). + +Hypothesis phi_le_p : forall v, (phi v) <= (p (val v)). + +Hypothesis p_cvx : (@convex_function R V [set: V] p). + +Definition extend_graph f := forall (v : F'), f (\val v) (phi v). + +Definition le_graph p f := + forall v r, f v r -> r <= p v. + +Definition functional_graph f := + forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. + +Definition linear_graph f := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + +Definition le_extend_graph f := + [/\ functional_graph f, linear_graph f, le_graph p f & extend_graph f]. + +Record zorn_type : Type := ZornType + {carrier : graph V; specP : le_extend_graph carrier}. + +Let spec_phi : le_extend_graph (fun v r => exists2 y : F', v = val y & r = phi y). +Proof. +split. +- by move=> v r1 r2 [y1 -> ->] [y2 + ->] => /val_inj ->. +- move => v1 v2 l r1 r2 [y1 -> ->] [y2 -> ->]. + by exists (y1 + l *: y2); rewrite !linearD !linearZ //. +- by move => r v [y -> ->]. +- by move => v; exists v. +Qed. + +Definition zphi := ZornType spec_phi. + +Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2. +Proof. +case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; move: pm1 pm2; rewrite e => pm1 pm2. +by congr ZornType; apply: Prop_irrelevance. +Qed. + +Definition zornS (z1 z2 : zorn_type):= + forall x y, (carrier z1 x y) -> (carrier z2 x y ). + + (* Zorn applied to the relation of extending the graph of the first function *) + Lemma zornS_ex : exists g : zorn_type, forall z, zornS g z -> z = g. + Proof. + pose Rbool := (fun x y => `[< zornS x y >]). + have RboolP : forall z t, Rbool z t <-> zornS z t by split; move => /asboolP //=. + suff [t st]: exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. + by exists t; move => z /RboolP tz; apply: st. + apply: (@Zorn zorn_type Rbool). + - by move => t; apply/RboolP. + - by move => r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b. + - move => r s /RboolP a /RboolP b; apply: zorn_type_eq. + by apply: funext => z; apply: funext => h;apply: propext; split => [/a | /b]. + - move => A Amax. + case: (lem (exists a, A a)) => [[w Aw] | eA]; last first. + by exists zphi => a Aa; elim: eA; exists a. + (* g is the union of the graphs indexed by elements in a *) + pose g v r := exists a, A a /\ (carrier a v r). + have g_fun : functional_graph g. + move=> v r1 r2 [a [Aa avr1]] [b [Ab bvr2]]. + have [] : Rbool a b \/ Rbool b a by exact: Amax. + - rewrite /Rbool /RboolP /zornS; case: b Ab bvr2 {Aa}. + move => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2. + by move/ecas2: avr1 => /fs2 /(_ s2vr2). + - rewrite /Rbool /RboolP /zornS; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. + by move/ecbs1: bvr2; apply: fs1. + have g_lin : linear_graph g. + move=> v1 v2 l r1 r2 [a1 [Aa1 c1]] [a2 [Aa2 c2]]. + have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2. + - have {c1 sc12 Aa1 a1} c1 : carrier a2 v1 r1 by apply: sc12. + exists a2; split=> //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. + - have {c2 sc21 Aa2 a2} c2 : carrier a1 v2 r2 by apply: sc21. + exists a1; split=> //; case: a1 {Aa1} c2 c1 => c /= [_ hl _ _] *; exact: hl. + have g_majp : le_graph p g by move=> v r [[c [fs1 ls1 ms1 ps1]]] /= [_ /ms1]. + have g_prol : extend_graph g. + move=> *; exists w; split=> //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp. + have spec_g : le_extend_graph g by split. + pose zg := ZornType spec_g. + by exists zg => [a Aa]; apply/RboolP; rewrite /zornS => v r cvr; exists a. + Qed. + + + Variable g : zorn_type. + + Hypothesis gP : forall z, zornS g z -> z = g. + + (*The next lemma proves that when z is of zorn_type, it can be extended on any + real line directed by an arbitrary vector v *) + + Lemma divDl_ge0 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : 0 <= s / (s +t). + by apply: divr_ge0 => //; apply: addr_ge0. + Qed. + + Lemma divDl_le1 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : s / (s +t) <= 1. + move: s0; rewrite le0r => /orP []; first by move => /eqP ->; rewrite mul0r //. + move: t0; rewrite le0r => /orP []. + by move => /eqP -> s0; rewrite addr0 divff //=; apply: lt0r_neq0. + by move=> t0 s0; rewrite ler_pdivrMr ?mul1r ?addr_gt0 // lerDl ltW. + Qed. + + Lemma divD_onem (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t). + rewrite /(_).~. + suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. + rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H. + by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW. + Qed. + + Lemma domain_extend (z : zorn_type) v : + exists2 ze : zorn_type, (zornS z ze) & (exists r, (carrier ze) v r). + Proof. + case: (lem (exists r, (carrier z v r))). + by case=> r rP; exists z => //; exists r. + case: z => [c [fs1 ls1 ms1 ps1]] /= nzv. + have c00 : c 0 0. + have <- : phi 0 = 0 by rewrite linear0. + by move: ps1; rewrite /extend_graph /= => /(_ 0) /=; rewrite GRing.val0; apply. + have [a aP] : exists a, forall (x : V) (r lambda : R), + c x r -> r + lambda * a <= p (x + lambda *: v). + suff [a aP] : exists a, forall (x : V) (r lambda : R), + c x r -> 0 < lambda -> + r + lambda * a <= p (x + lambda *: v) /\ + r - lambda * a <= p (x - lambda *: v). + exists a=> x r lambda cxr. + have {aP} aP := aP _ _ _ cxr. + case: (ltrgt0P lambda) ; [by case/aP | move=> ltl0 | move->]; last first. + by rewrite mul0r scale0r !addr0; apply: ms1. + rewrite -[lambda]opprK scaleNr mulNr. + have /aP [] : 0 < - lambda by rewrite oppr_gt0. + done. + pose b (x : V) r lambda : R := (p (x + lambda *: v) - r) / lambda. + pose a (x : V) r lambda : R := (r - p (x - lambda *: v)) / lambda. + have le_a_b x1 x2 r1 r2 s t : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t -> + a x1 r1 s <= b x2 r2 t. + move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b. + rewrite ler_pdivlMr // mulrAC ler_pdivrMr // mulrC [_ * s]mulrC. + rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr. + have /ler_pM2r <- : 0 < (s + t) ^-1 by rewrite invr_gt0 addr_gt0. + set y1 : V := _ + _ *: _; set y2 : V := _ - _ *: _. + set rhs := (X in _ <= X). + have step1 : p (s / (s + t) *: y1 + t / (s + t) *: y2) <= rhs. + rewrite /rhs !mulrDl ![_ * _ / _]mulrAC. + pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t)) ((divDl_le1 (ltW lt0s) (ltW lt0t))). + move: (p_cvx st (in_setT y1) (in_setT y2)). + by rewrite /conv /= [X in ((_ <= X)-> _)]/conv /= divD_onem /=. + apply: le_trans step1 => {rhs}. + set u : V := (X in p X). + have {u y1 y2} -> : u = t / (s + t) *: x1 + s / (s + t) *: x2. + rewrite /u ![_ / _]mulrC -!scalerA -!scalerDr /y1 /y2; congr (_ *: _). + by rewrite !scalerDr addrCA scalerN scalerA [s * t]mulrC -scalerA addrK. + set l := t / _; set m := s / _; set lhs := (X in X <= _). + have {lhs} -> : lhs = l * r1 + m * r2. + by rewrite /lhs mulrDl ![_ * _ / _]mulrAC. + apply: ms1; apply: (ls1) => //. + rewrite -[_ *: _]add0r -[_ * _] add0r; apply: ls1 => //. + pose Pa : set R := fun r => exists x1, exists r1, exists s1, + [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]. + pose Pb : set R := fun r => exists x1, exists r1, exists s1, + [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]. + pose sa := reals.sup Pa. (* This is why we need realTypes, we need p with values in a realType *) + have Pax : Pa !=set0 by exists (a 0 0 1); exists 0; exists 0; exists 1; split. + have ubdP : ubound Pa sa. + apply: sup_upper_bound; split => //=. + exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have saP: forall u : R, ubound Pa u -> sa <= u by move=> u; apply: ge_sup. + pose ib := reals.inf Pb. (* This is why we need realTypes, we need P with values in a realType *) + have Pbx : Pb !=set0 by exists (b 0 0 1); exists 0; exists 0; exists 1; split. + have ibdP : lbound Pb ib. + by apply: ge_inf; exists (a 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have ibP: forall u : R, lbound Pb u -> u <= ib by move=> u; apply: lb_le_inf Pbx. + have le_sa_ib : sa <= ib. + apply: saP=> r' [y [r [l [cry lt0l -> {r'}]]]]. + apply: ibP=> s' [z [s [m [crz lt0m -> {s'}]]]]; exact: le_a_b. + pose alpha := ((sa + ib) / 2%:R). + have le_alpha_ib : alpha <= ib by rewrite /alpha midf_le. + have le_sa_alpha : sa <= alpha by rewrite /alpha midf_le. + exists alpha => x r l cxr lt0l; split. + - suff : alpha <= b x r l. + by rewrite /b; move/ler_pdivlMr: lt0l->; rewrite lerBrDl mulrC. + by apply: le_trans le_alpha_ib _; apply: ibdP; exists x; exists r; exists l. + - suff : a x r l <= alpha. + rewrite /a. move/ler_pdivrMr: lt0l->. + by rewrite lerBlDl -lerBlDr mulrC. + by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l. + pose z' := fun k r => + exists v' : V, exists r' : R, exists lambda : R, + [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a]. + have z'_extends : forall v r, c v r -> z' v r. + move=> x r cxr; exists x; exists r; exists 0; split=> //. + - by rewrite scale0r addr0. + - by rewrite mul0r addr0. + have z'_prol : extend_graph z'. + move=> x; exists (val x); exists (phi x); exists 0; split=> //. + - by rewrite scale0r addr0. + - by rewrite mul0r addr0. + - have z'_maj_by_p : le_graph p z'. + by move=> x r [w [s [l [cws -> ->]]]]; apply: aP. + - have z'_lin : linear_graph z'. + move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]]. + set w := (X in z' X _); set s := (X in z' _ X). + have {w} -> : w = w1 + l *: w2 + (m1 + l * m2) *: v. + by rewrite /w !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA. + have {s} -> : s = s1 + l * s2 + (m1 + l * m2) * a. + by rewrite /s !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA. + exists (w1 + l *: w2); exists (s1 + l * s2); exists (m1 + l * m2); split=> //. + exact: ls1. + - have z'_functional : functional_graph z'. + move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]]. + have h1 (x : V) (r l : R) : x = l *: v -> c x r -> x = 0 /\ l = 0. + move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r. + suff cvs: c v (l^-1 * r) by elim:nzv; exists (l^-1 * r). + suff -> : v = l ^-1 *: (l *: v). + have -> : + c ( l ^-1 *: (l *: v)) (l^-1 * r) = + c (0 + l ^-1 *: (l *: v)) (0 + l^-1 * r) by rewrite !add0r. + by apply: ls1=> //; apply: linrel_00 fxr. + by rewrite scalerA mulVf ?scale1r. + have [rw12 erw12] : exists r, c (w1 - w2) r. + exists (s1 + (-1) * s2). + have -> : w1 - w2 = w1 + (-1) *: w2 by rewrite scaleNr scale1r. + by apply: ls1. + have [ew12 /eqP]: w1 - w2 = 0 /\ (m2 - m1 = 0). + apply: h1 erw12; rewrite scalerBl; apply/eqP; rewrite subr_eq addrC addrA. + by rewrite -subr_eq opprK e1. + suff -> : s1 = s2 by rewrite subr_eq0=> /eqP->. + by apply: fs1 cws2; move/eqP: ew12; rewrite subr_eq0=> /eqP<-. + have z'_spec : le_extend_graph z' by split. + pose zz' := ZornType z'_spec. + exists zz'; rewrite /zornS => //=; exists a; exists 0; exists 0; exists 1. + by rewrite add0r mul1r scale1r add0r; split. + Qed. + + Let tot_g v : exists r, carrier g v r. + Proof. + have [z /gP sgz [r zr]]:= domain_extend g v. + by exists r; rewrite -sgz. + Qed. + + +Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r). +Proof. +move: (choice tot_g) => [h hP]; exists h => v r; split; last by move<-. +case: g gP tot_g hP => c /= [fg lg mg pg] => gP' tot_g' hP cvr. +by have -> // := fg v r (h v). +Qed. + + + End HBPreparation. + + +Section HahnBanach. +Import Lingraph. +(* Now we prove HahnBanach on functions*) +(* We consider R a real (=ordered) field with supremum, and V a (left) module + on R. We do not make use of the 'vector' interface as the latter enforces + finite dimension. *) + + Variables (R : realType) (V : lmodType R) (F : pred V). + + Variables (F' : subLmodType F) (f : {linear F' -> R}) (p : V -> R). + + +(* MathComp seems to lack of an interface for submodules of V, so for now + we state "by hand" that F is closed under linear combinations. *) + +Hypothesis p_cvx : (@convex_function R V [set: V] p). + +Hypothesis f_bounded_by_p : forall (z : F'), (f z <= p (\val z)). + +Theorem HahnBanach : exists g : {scalar V}, + (forall x, g x <= p x) /\ (forall (z : F'), g (\val z) = f z). +Proof. +pose graphF (v : V) r := exists2 z : F', v = \val z & r = f z. +have [z zmax]:= zornS_ex f_bounded_by_p. +have [g gP]:= (hb_witness p_cvx zmax). +have scalg : linear_for *%R g. + case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. + have addg : additive g. + by move=> w1 w2; apply/gP; apply: lingraph_add =>//; apply/gP. + suff scalg : scalable_for *%R g. + by move=> a u v; rewrite -gP (addrC _ v) (addrC _ (g v)); apply: ls1; apply /gP. + by move=> w l; apply/gP; apply: lingraph_scale=> //; apply/gP. +pose H := GRing.isLinear.Build _ _ _ _ g scalg. +pose g' : {linear V -> R | *%R} := HB.pack g H. +exists g'. +split; last first. + by move => z'; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. +by case: z {zmax} gP => [c [_ _ bp _]] /= gP => x; apply: bp; apply/gP. +Qed. + +End HahnBanach. + + +(* To add once this is rebased over linear_continuous *) +(* Section Substructures. *) +(* Context (R: numFieldType) (V : normedModType R). *) +(* Variable (A : pred V). *) + +(* HB.instance Definition _ := NormedModule.on (subspace A). *) + +(* Check {linear_continuous (subspace A) -> R^o}. *) + +(* End Substructures. *) + +Section HBGeom. + +Variable (R : realType) (V : normedModType R) (F : pred V) +(F' : subLmodType F) (f : {linear F' -> R}). + +(* once this is rebased over linear_continuous +Variable (R : realType) (V : normedModType R) (F : pred V) +(f : {linear_continuous (subspace F) -> R}). +*) + +Let setF := [set x : V | exists (z : F'), val z = x]. + +Theorem HB_geom_normed : + exists r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <= `|(val z)| * r)) -> +(* hypothesis to delete once this is rebased over linear_continuous + and obtain through continuous_linear_bounded *) + exists g: {linear_continuous V -> R}, (forall x : V, F x -> (g x = f x)). +Proof. + move=> [r [ltr0 fxrx]]. + pose p:= fun x : V => `|x|*r. + have convp: (@convex_function _ _ [set: V] p). + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [X in (_ <= X)]/conv /= /p. + apply: le_trans. + have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. + by apply: ler_normD. + by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. + rewrite mulrDl !normrZ -![_ *: _]/(_ * _). + have -> : `|l%:num| = l%:num by apply/normr_idP. + have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0. + by rewrite !mulrA. + have majfp : forall z : F', f z <= p (\val z). + move => z; rewrite /(p _) ; apply : le_trans; last by []. + by apply : ler_norm. + move: (HahnBanach convp majfp) => [ g [majgp F_eqgf] ] {majfp}. + exists g; split; last by []. + move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). + apply: bounded_linear_continuous. + exists r. + split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *) + move => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. + move => y; rewrite -ball_normE //= sub0r => y1. + rewrite ler_norml; apply/andP. split. + - rewrite lerNl -linearN; apply: (le_trans (majgp (-y))). + by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. + - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. + apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. +Qed. + +End HBGeom. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 7e69d4b3f..4dfe4a212 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -49,7 +49,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a *) (* convex tvs from an Lmodule which is also a *) (* topological space *) -(* ``` *) (* HB instances: *) (* - The type R^o (R : numFieldType) is endowed with the structure of *) (* ConvexTvs. *) @@ -511,6 +510,7 @@ Unshelve. all: by end_near. Qed. Local Open Scope convex_scope. + Let standard_ball_convex_set (x : R^o) (r : R) : convex_set (ball x r). Proof. apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. @@ -603,3 +603,182 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex. End prod_ConvexTvs. + +HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) + (F : NbhsZmodule.type) (s : K -> F -> F) := + {f of @GRing.Linear K E F s f & @Continuous E F f }. + +(* https://github.com/math-comp/math-comp/issues/1536 + we use GRing.Scale.law even though it is claimed to be internal *) +HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) + (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := { + linearP : linear_for s f ; + continuousP : continuous f + }. + +HB.builders Context K E F s f of @isLinearContinuous K E F s f. + +HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP. +HB.instance Definition _ := isContinuous.Build E F f continuousP. + +HB.end. + +Section lcfun_pred. +Context {K : numDomainType} {E : NbhsLmodule.type K} {F : NbhsZmodule.type} {s : K -> F -> F}. +Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ]. +Definition lcfun_key : pred_key lcfun. Proof. exact. Qed. +Canonical lcfun_keyed := KeyedPred lcfun_key. + +End lcfun_pred. + +Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'" + (at level 0, U at level 98, V at level 99, + format "{ 'linear_continuous' U -> V | s }"). +Reserved Notation "'{' 'linear_continuous' U '->' V '}'" + (at level 0, U at level 98, V at level 99, + format "{ 'linear_continuous' U -> V }"). +Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s) + : type_scope. +Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R} + : type_scope. + +Section lcfun. +Context {R : numDomainType} {E : NbhsLmodule.type R} + {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. +Notation T := {linear_continuous E -> F | s}. +Notation lcfun := (@lcfun _ E F s). + +Section Sub. +Context (f : E -> F) (fP : f \in lcfun). + +Definition lcfun_Sub_subproof := + @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)). +#[local] HB.instance Definition _ := lcfun_Sub_subproof. +Definition lcfun_Sub : {linear_continuous _ -> _ | _ } := f. +End Sub. + +Lemma lcfun_rect (K : T -> Type) : + (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u. +Proof. +move=> Ksub [f [[Pf1] [Pf2] [Pf3]]]. +set G := (G in K G). +have Pf : f \in lcfun. + by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2. +suff -> : G = lcfun_Sub Pf by apply: Ksub. +rewrite {}/G. +congr (LinearContinuous.Pack (LinearContinuous.Class _ _ _)). +- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance. +- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance. +- by congr isContinuous.Axioms_; exact: Prop_irrelevance. +Qed. + +Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP. + +Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:]. + +Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type := + | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true. + +Lemma lcfunP (f : E -> F) : f \in lcfun -> lcfun_spec f f (f \in lcfun). +Proof. +move=> /[dup] f_lc ->. +have {2}-> : f = lcfun_Sub f_lc by rewrite lcfun_valP. +by constructor. +Qed. + +End lcfun. + +Section lcfun_comp. + +Context {R : numDomainType} {E F : NbhsLmodule.type R} + {S : NbhsZmodule.type} {s : GRing.Scale.law R S} + (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}). + +Let lcfun_comp_subproof1 : linear_for s (g \o f). +Proof. by move=> *; move=> *; rewrite !linearP. Qed. + +Let lcfun_comp_subproof2 : continuous (g \o f). +Proof. by move=> x; apply: continuous_comp; exact/cts_fun. Qed. + +HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) + lcfun_comp_subproof1 lcfun_comp_subproof2. + +End lcfun_comp. + +Section lcfun_lmodtype. +Context {R : numFieldType} {E F : convexTvsType R}. +Implicit Types (r : R) (f g : {linear_continuous E -> F}). + +Import GRing.Theory. + +Lemma null_fun_continuous : continuous (\0 : E -> F). +Proof. +by apply: cst_continuous. +Qed. + +HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous. + +(** NB : cvgD in pseudometric_normedZmodule could be lowered to some common + structure to convexTvsType and pseudometric, then `lcfun_cvgD` doesn't need to + exist anymore (we are however not sure that this deserves the introduction of + a new structure that combines nbhs and normedZmodule) *) +Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b : + f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. +Proof. +move=> fa ga. +by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..]. +Qed. + +Lemma lcfun_continuousD f g : continuous (f \+ g). +Proof. by move=> /= x; apply: lcfun_cvgD; exact: cts_fun. Qed. + +Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a : + f @ U --> a -> \- f @ U --> - a. +Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed. + +Lemma lcfun_continuousN f : continuous (\- f). +Proof. by move=> /= x; apply: lcfun_cvgN; exact: cts_fun. Qed. + +HB.instance Definition _ f g := + isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g). + +Lemma lcfun_cvgZ (U : set_system E) {FF : Filter U} l f r a : + l @ U --> r -> f @ U --> a -> + l x *: f x @[x --> U] --> r *: a. +Proof. +by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)). +Qed. + +Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : + f @ U --> a -> k \*: f @ U --> k *: a. +Proof. by apply: lcfun_cvgZ => //; exact: cvg_cst. Qed. + +Lemma lcfun_continuousM r g : continuous (r \*: g). +Proof. by move=> /= x; apply: lcfun_cvgZr; exact: cts_fun. Qed. + +HB.instance Definition _ r g := + isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g). + +Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R). +Proof. +split; first by rewrite inE; split; first apply/linearP; exact: cst_continuous. +move=> r /= _ _ /lcfunP[f] /lcfunP[g]. +by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD]. +Qed. + +HB.instance Definition _ f := + isContinuous.Build E F (\- f) (@lcfun_continuousN f). + +HB.instance Definition _ := + @GRing.isSubmodClosed.Build _ _ lcfun lcfun_submod_closed. + +HB.instance Definition _ := + [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:]. + +End lcfun_lmodtype. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index c5c087cc1..e3ab10cad 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -260,11 +260,6 @@ move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA]. by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA]. Qed. -Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x : - {for x, continuous f} -> {for (f x), continuous g} -> - {for x, continuous (g \o f)}. -Proof. exact: cvg_comp. Qed. - Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D). Proof.