Theorems · Theorem · general topology

PseudoEpimorphism.mk.sizeOf_spec

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

Defined in

Mathlib.Topology.Order.Hom.Esakia

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

PreorderPreorderSizeOfSizeOf