Theorems · Theorem · general topology

EsakiaHom.mk.sizeOf_spec

∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toContinuousOrderHom : α →Co β)
  (exists_map_eq_of_map_le' :
    ∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom.toFun c = b),
  sizeOf { toContinuousOrderHom := toContinuousOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } =
    1 + sizeOf toContinuousOrderHom

Defined in

Mathlib.Topology.Order.Hom.Esakia

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

TopologicalSpacePreorderTopologicalSpacePreorderSizeOfSizeOf