Experiment : Tvs#1846

Draft

mkerjean wants to merge 28 commits intomath-comp:masterfrom

mkerjean:topdual

Commits on Feb 18, 2026

put convex.v lower in the file hier
affeldt-aist
committed
LinearContinuous structure

mkerjean
authored and
affeldt-aist
committed
wip duality

CohenCyril
authored and
affeldt-aist
committed
HB saturate bug

mkerjean
authored and
affeldt-aist
committed
fail lcfun_rect

mkerjean
authored and
affeldt-aist
committed
missing join

mkerjean
authored and
affeldt-aist
committed
bornology wip

mkerjean
authored and
affeldt-aist
committed
lcfun_lmodtype and lcfun_topologicaltype

mkerjean
authored and
affeldt-aist
committed
wip lcfun_topologicaltype

mkerjean
authored and
affeldt-aist
committed
fix by @affeldt-aist

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
end lcfun_lmodtype with Cyril

mkerjean
authored and
affeldt-aist
committed
notations

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
wip

mkerjean
authored and
affeldt-aist
committed
change name to ConvexTvs and ctvs

mkerjean
authored and
affeldt-aist
committed
wip bornology

mkerjean
authored and
affeldt-aist
committed
copy hahn banach from old branch, does not compile yet
affeldt-aist
committed
use convex that has just been split
affeldt-aist
committed
wip
affeldt-aist
committed
update hahnbanach, delete admit wip
mkerjean
committed

Commits on Feb 19, 2026