Mathlib Map

Theorems · Definition · order theory

sInfHom.toFun

{α : Type u_8} → {β : Type u_9} → [inst : InfSet α] → [inst_1 : InfSet β] → sInfHom α β → α → β

The underlying function of an sInfHom.

Defined in
Mathlib.Order.Hom.CompleteLattice
Cited by
8 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
InfSetInfSet
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CompleteLatticeHom.mk.inj · cited by 1mk.injCompleteLatticeHom.mk.noConfusion · cited by 1mk.noConfusionCompleteLatticeHom.tosSupHom · cited by 1CompleteLatticeHom.tosSup…sInfHom.map_sInf' · cited by 1sInfHom.map_sInf'CompleteLatticeHom.map_sSup' · cited by 1CompleteLatticeHom.map_sS…CompleteLatticeHom.noConfusion · cited by 0CompleteLatticeHom.noConf…CompleteLatticeHom.noConfusionType · cited by 0CompleteLatticeHom.noConf…CompleteLatticeHom.mk.injEq · cited by 0mk.injEqCompleteLatticeHom.recOn · cited by 0CompleteLatticeHom.recOnCompleteLatticeHom.mk.sizeOf_spec · cited by 0mk.sizeOf_specCompleteLatticeHom.toFun_eq_coe · cited by 0CompleteLatticeHom.toFun_…sInfHom.toFun_eq_coe · cited by 0sInfHom.toFun_eq_coeCompleteLatticeHom.casesOn · cited by 0CompleteLatticeHom.casesOnCompleteLatticeHom.coe_mk · cited by 0CompleteLatticeHom.coe_mkInfSet · cited by 145InfSetsInfHom · cited by 43sInfHomsInfHom.toFunCITED BYCITES

Cites2

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

  • InfSetstatement and proof · cited by 145
  • sInfHomstatement and proof · cited by 43

Cited by14

Results whose statement or proof uses this declaration.