Theorems · Theorem · general topology

IsLocalMin.sup

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] {f g : α → β} {a : α},
  IsLocalMin f a → IsLocalMin g a → IsLocalMin (fun x => f x ⊔ g x) a

Defined in: Mathlib.Topology.Order.LocalExtr
Cited by: 0 results in Mathlib
Foundations: Depth 20 from the axioms · uses propext, Quot.sound
Assumes: TopologicalSpace SemilatticeSup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
SemilatticeSupstatement and proof · cited by 785
IsLocalMinstatement and proof · cited by 45
IsMinFilter.supproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.