Theorems · Theorem · order theory

Set.toFinset_Iio

∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α) [inst_2 : Fintype ↑(Set.Iio a)],
  (Set.Iio a).toFinset = Finset.Iio a

Defined in

Mathlib.Order.Interval.Finset.Defs

Cited by

2 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderLocallyFiniteOrderBotFintype