@[reducible, inline]

abbrev Set.interIio {β : Type u_1} [Preorder β] (S : Set β) (b : β) : Set β

Given a set S and an element b in an order β, Set.interIio S b A is the intersection S ∩ Iio b.

Equations

• S.interIio b = S ∩ Set.Iio b

@[reducible, inline]

abbrev Set.interIcc {β : Type u_1} [Preorder β] [OrderBot β] (S : Set β) (a b : β) : Set β

Given a set S and elements a and b in an order β, Set.interIcc S a b is the intersection S ∩ Icc a b.

Equations

• S.interIcc a b = S ∩ Set.Icc a b

theorem Set.finite_interIio {β : Type u_1} [Preorder β] {S : Set β} {b : β} [LocallyFiniteOrderBot β] : (S.interIio b).Finite

noncomputable instance instFintypeElemInterIioOfLocallyFiniteOrderBot {β : Type u_1} [Preorder β] (S : Set β) (b : β) [LocallyFiniteOrderBot β] : Fintype ↑(S.interIio b)

Equations

• instFintypeElemInterIioOfLocallyFiniteOrderBot S b = ⋯.fintype

theorem Set.finite_interIcc {β : Type u_1} [Preorder β] {S : Set β} {a b : β} [LocallyFiniteOrder β] [OrderBot β] : (S.interIcc a b).Finite

noncomputable instance instFintypeElemInterIccOfLocallyFiniteOrder {β : Type u_1} [Preorder β] (S : Set β) (a b : β) [LocallyFiniteOrder β] [OrderBot β] : Fintype ↑(S.interIcc a b)

Equations

• instFintypeElemInterIccOfLocallyFiniteOrder S a b = ⋯.fintype

@[simp]

theorem Set.interIio_univ {β : Type u_1} [Preorder β] (b : β) : univ.interIio b = Iio b

@[simp]

theorem Set.interIio_univ' {β : Type u_1} [Preorder β] (b : β) : univ.interIio b = Iio b

@[simp]

theorem Set.interIio_empty {β : Type u_1} [Preorder β] (b : β) : ∅.interIio b = ∅

theorem Set.interIio_mono {β : Type u_1} [Preorder β] {S T : Set β} (h : S ⊆ T) (b : β) : S.interIio b ⊆ T.interIio b