Support

📁 Source: Mathlib/Topology/Algebra/Order/Support.lean

Statistics

Metric	Count
Definitions	0
Theorems inf, sup, inf, sup	4
Total	4

HasCompactMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	HasCompactMulSupport	Pi.instMinForall_mathlib SemilatticeInf.toMin	—	IsCompact.of_isClosed_subset IsCompact.union isClosed_mulTSupport mulTSupport.eq_1 closure_union closure_mono Function.mulSupport_inf
sup 📖	mathematical	HasCompactMulSupport	Pi.instMaxForall_mathlib SemilatticeSup.toMax	—	IsCompact.of_isClosed_subset IsCompact.union isClosed_mulTSupport mulTSupport.eq_1 closure_union closure_mono Function.mulSupport_sup

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	HasCompactSupport	Pi.instMinForall_mathlib SemilatticeInf.toMin	—	IsCompact.of_isClosed_subset IsCompact.union isClosed_tsupport tsupport.eq_1 closure_union closure_mono Function.support_inf
sup 📖	mathematical	HasCompactSupport	Pi.instMaxForall_mathlib SemilatticeSup.toMax	—	IsCompact.of_isClosed_subset IsCompact.union isClosed_tsupport tsupport.eq_1 closure_union closure_mono Function.support_sup

---

← Back to Index