Topology lemmas#2014

Open

Brixfoly wants to merge 30 commits into

math-comp:masterfrom

Brixfoly:topology_lemmas

Commits on Jun 29, 2026

reduce dep
affeldt-aist
committed

Commits on Jun 30, 2026

Commits on Jul 1, 2026

added cvg_mu lemmas + sigma_algebra_subl
adjevahi
committed
fix

affeldt-aist
authored and
adjevahi
committed
added preimageD
adjevahi
committed
actually use preimageD1

affeldt-aist
authored and
adjevahi
committed
added sub_sigma_algebra_measurable and subset_g_sigma_algebra
adjevahi
committed
added cvg_mu lemmas + sigma_algebra_subl
adjevahi
committed
rebase
adjevahi
committed
rebase + added cvg_mu and sigma_algebra_subl
adjevahi
committed
fix

affeldt-aist
authored and
adjevahi
committed
added preimageD
adjevahi
committed
cleanup
adjevahi
committed
fix
affeldt-aist
committed
added countable_big(a/u)p measurable
adjevahi
committed
changelog
affeldt-aist
committed
fix
affeldt-aist
committed
make normed module depends on metric

affeldt-aist
authored and
adjevahi
committed
fix

affeldt-aist
authored and
adjevahi
committed
fix

affeldt-aist
authored and
adjevahi
committed
make normed module depends on metric

affeldt-aist
authored and
adjevahi
committed
fix

affeldt-aist
authored and
adjevahi
committed
fix

affeldt-aist
authored and
adjevahi
committed
Merge branch 'metric_20260629' of https://github.com/affeldt-aist/analysis into metric_20260629
adjevahi
committed
added separable def, +sigma algebras generated by basis
adjevahi
committed
added measurable_topology
adjevahi
committed
Merge branch 'master' into topology_lemmas
Brixfoly
authored

Commits on Jul 2, 2026

added <<s open>> = <<s ocitv>>
adjevahi
committed