Theorems · Theorem · functional analysis

absConvex_closed_sInter

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {S : Set (Set E)},
  (∀ s ∈ S, AbsConvex 𝕜 s ∧ IsClosed s) → AbsConvex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)

Defined in: Mathlib.Analysis.LocallyConvex.AbsConvex
Cited by: 0 results in Mathlib
Foundations: Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: SeminormedRing SMul AddCommMonoid PartialOrder TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
AddCommMonoidstatement and proof · cited by 12,281
PartialOrderstatement and proof · cited by 6,410
IsClosedstatement and proof · cited by 1,639
SeminormedRingstatement and proof · cited by 446
Set.sInterstatement · cited by 225
AbsConvexstatement and proof · cited by 31
isClosed_sInterproof · cited by 10
AbsConvex.sInterproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

closedAbsConvexHullproof · cited by 10