Theorems · Theorem · general topology

sInfHom.continuous

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] [inst_2 : TopologicalSpace α]
  [Topology.IsLower α] [inst_4 : TopologicalSpace β] [Topology.IsLower β] (f : sInfHom α β), Continuous ⇑f

Defined in: Mathlib.Topology.Order.LowerUpperTopology
Cited by: 1 results in Mathlib
Foundations: Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CompleteLattice CompleteLattice TopologicalSpace Topology.IsLower TopologicalSpace Topology.IsLower

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites21

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

DFunLike.coestatement and proof · cited by 62,936
Setproof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.preimageproof · cited by 4,946
LE.le.transproof · cited by 3,151
Continuousstatement · cited by 2,592
IsClosedproof · cited by 1,639
Set.Iciproof · cited by 1,070
CompleteLatticestatement and proof · cited by 1,048
le_transproof · cited by 985
InfSet.sInfproof · cited by 935
Eq.geproof · cited by 375

Cited by1

Results whose statement or proof uses this declaration.

sSupHom.continuousproof · cited by 0