Mathlib Map

Theorems · Definition · order theory

InfTopHom.toInfHom

{α : Type u_6} →
  {β : Type u_7} → [inst : Min α] → [inst_1 : Min β] → [inst_2 : Top α] → [inst_3 : Top β] → InfTopHom α β → InfHom α β
Defined in
Mathlib.Order.Hom.BoundedLattice
Cited by
10 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
MinMinTopTop
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

InfTopHom.comp · cited by 12InfTopHom.compInfTopHom.dual · cited by 5InfTopHom.dualSupBotHom.dual · cited by 5SupBotHom.dualInfTopHom.copy · cited by 2InfTopHom.copyFrameHom.mk.inj · cited by 1mk.injFrameHom.mk.noConfusion · cited by 1mk.noConfusionInfTopHom.toTopHom · cited by 1InfTopHom.toTopHomFrameHom.coe_mk · cited by 0FrameHom.coe_mkFrameHom.map_sSup' · cited by 0FrameHom.map_sSup'InfTopHom.coe_toInfHom · cited by 0InfTopHom.coe_toInfHomFrameHom.noConfusion · cited by 0FrameHom.noConfusionFrameHom.noConfusionType · cited by 0FrameHom.noConfusionTypeFrameHom.recOn · cited by 0FrameHom.recOnFrameHom.toFun_eq_coe · cited by 0FrameHom.toFun_eq_coeFrameHom.mk.congr_simp · cited by 0mk.congr_simpTop · cited by 93TopInfHom · cited by 69InfHomInfTopHom · cited by 60InfTopHomInfTopHom.toInfHomCITED BYCITES

Cites3

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

  • Topstatement and proof · cited by 93
  • InfHomstatement · cited by 69
  • InfTopHomstatement and proof · cited by 60

Cited by20

Results whose statement or proof uses this declaration.