Order structures on finite types

This file provides order instances on fintypes.

Computable instances

On a Fintype, we can construct

• an OrderBot from SemilatticeInf.
• an OrderTop from SemilatticeSup.
• a BoundedOrder from Lattice.

Those are marked as def to avoid defeqness issues.

Completion instances

Those instances are noncomputable because the definitions of sSup and sInf use Set.toFinset and set membership is undecidable in general.

On a Fintype, we can promote:

• a Lattice to a CompleteLattice.
• a DistribLattice to a CompleteDistribLattice.
• a LinearOrder to a CompleteLinearOrder.
• a BooleanAlgebra to a CompleteAtomicBooleanAlgebra.

Those are marked as def to avoid typeclass loops.

Concrete instances

We provide a few instances for concrete types:

• Fin.completeLinearOrder
• Bool.completeLinearOrder
• Bool.completeBooleanAlgebra

@[reducible, inline]

abbrev Fintype.toOrderBot (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeInf α] : OrderBot α

Constructs the ⊥ of a finite nonempty SemilatticeInf.

Equations

• Fintype.toOrderBot α = { bot := Finset.univ.inf' ⋯ id, bot_le := ⋯ }

@[reducible, inline]

abbrev Fintype.toOrderTop (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeSup α] : OrderTop α

Constructs the ⊤ of a finite nonempty SemilatticeSup

Equations

• Fintype.toOrderTop α = { top := Finset.univ.sup' ⋯ id, le_top := ⋯ }

@[reducible, inline]

abbrev Fintype.toBoundedOrder (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] : BoundedOrder α

Constructs the ⊤ and ⊥ of a finite nonempty Lattice.

Equations

• Fintype.toBoundedOrder α = { toOrderTop := Fintype.toOrderTop α, toOrderBot := Fintype.toOrderBot α }

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteLattice (α : Type u_2) [Fintype α] [Lattice α] [BoundedOrder α] : CompleteLattice α

A finite bounded lattice is complete.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteDistribLatticeMinimalAxioms (α : Type u_2) [Fintype α] [DistribLattice α] [BoundedOrder α] : CompleteDistribLattice.MinimalAxioms α

A finite bounded distributive lattice is completely distributive.

Equations

• Fintype.toCompleteDistribLatticeMinimalAxioms α = { toCompleteLattice := Fintype.toCompleteLattice α, inf_sSup_le_iSup_inf := ⋯, iInf_sup_le_sup_sInf := ⋯ }

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteDistribLattice (α : Type u_2) [Fintype α] [DistribLattice α] [BoundedOrder α] : CompleteDistribLattice α

A finite bounded distributive lattice is completely distributive.

Equations

• Fintype.toCompleteDistribLattice α = CompleteDistribLattice.ofMinimalAxioms (Fintype.toCompleteDistribLatticeMinimalAxioms α)

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteLinearOrder (α : Type u_2) [Fintype α] [LinearOrder α] [BoundedOrder α] : CompleteLinearOrder α

A finite bounded linear order is complete.

If the α is already a BiheytingAlgebra, then prefer to construct this instance manually using Fintype.toCompleteLattice instead, to avoid creating a diamond with LinearOrder.toBiheytingAlgebra.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteBooleanAlgebra (α : Type u_2) [Fintype α] [BooleanAlgebra α] : CompleteBooleanAlgebra α

A finite Boolean algebra is complete.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteAtomicBooleanAlgebra (α : Type u_2) [Fintype α] [BooleanAlgebra α] : CompleteAtomicBooleanAlgebra α

A finite Boolean algebra is complete and atomic.

Equations

• Fintype.toCompleteAtomicBooleanAlgebra α = CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteLatticeOfNonempty (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] : CompleteLattice α

A nonempty finite lattice is complete. If the lattice is already a BoundedOrder, then use Fintype.toCompleteLattice instead, as this gives definitional equality for ⊥ and ⊤.

Equations

• Fintype.toCompleteLatticeOfNonempty α = Fintype.toCompleteLattice α

@[reducible, inline]

noncomputable abbrev Fintype.toCompleteLinearOrderOfNonempty (α : Type u_2) [Fintype α] [Nonempty α] [LinearOrder α] : CompleteLinearOrder α

A nonempty finite linear order is complete. If the linear order is already a BoundedOrder, then use Fintype.toCompleteLinearOrder instead, as this gives definitional equality for ⊥ and ⊤.

Equations

• Fintype.toCompleteLinearOrderOfNonempty α = Fintype.toCompleteLinearOrder α

Concrete instances

@[instance_reducible]

noncomputable instance Fin.completeLinearOrder {n : ℕ} [NeZero n] : CompleteLinearOrder (Fin n)

Equations

• Fin.completeLinearOrder = Fintype.toCompleteLinearOrder (Fin n)

@[instance_reducible]

noncomputable instance Bool.completeBooleanAlgebra : CompleteBooleanAlgebra Bool

Equations

• Bool.completeBooleanAlgebra = Fintype.toCompleteBooleanAlgebra Bool

@[instance_reducible]

noncomputable instance Bool.completeLinearOrder : CompleteLinearOrder Bool

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Bool.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Bool

Equations

• Bool.completeAtomicBooleanAlgebra = Fintype.toCompleteAtomicBooleanAlgebra Bool

Directed Orders

theorem Directed.finite_set_le {α : Type u_2} {r : α → α → Prop} [IsTrans α r] {γ : Type u_3} [Nonempty γ] {f : γ → α} (D : Directed r f) {s : Set γ} (hs : s.Finite) : ∃ (z : γ), ∀ i ∈ s, r (f i) (f z)

theorem Directed.finite_le {α : Type u_2} {r : α → α → Prop} [IsTrans α r] {ι : Sort u_4} {κ : Sort u_5} [Nonempty ι] [Finite κ] {f : ι → α} (hf : Directed r f) (g : κ → ι) : ∃ (z : ι), ∀ (i : κ), r (f (g i)) (f z)

theorem Finite.exists_le {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [Preorder α] [IsDirectedOrder α] (f : ι → α) : ∃ (M : α), ∀ (i : ι), f i ≤ M

theorem Finite.exists_ge {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [Preorder α] [IsCodirectedOrder α] (f : ι → α) : ∃ (M : α), ∀ (i : ι), M ≤ f i

theorem Set.Finite.exists_le {α : Type u_2} [Nonempty α] [Preorder α] [IsDirectedOrder α] {s : Set α} (hs : s.Finite) : ∃ (M : α), ∀ i ∈ s, i ≤ M

theorem Set.Finite.exists_ge {α : Type u_2} [Nonempty α] [Preorder α] [IsCodirectedOrder α] {s : Set α} (hs : s.Finite) : ∃ (M : α), ∀ i ∈ s, M ≤ i

@[simp]

theorem Finite.bddAbove_range {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [Preorder α] [IsDirectedOrder α] (f : ι → α) : BddAbove (Set.range f)

@[simp]

theorem Finite.bddBelow_range {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [Preorder α] [IsCodirectedOrder α] (f : ι → α) : BddBelow (Set.range f)

theorem le_iSup_iff_of_directed {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} {f : ι → α} [Nonempty ι] [Finite ι] (hf : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) : a ≤ ⨆ (i : ι), f i ↔ ∃ (i : ι), a ≤ f i

theorem le_sSup_iff_of_directedOn {α : Type u_2} [CompleteLattice α] {s : Set α} {a : α} (hs : s.Nonempty) (hs' : s.Finite) (hs'' : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) : a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

theorem Set.subset_iUnion_iff_of_directed {ι : Sort u_1} {α : Type u_2} {s : Set α} {f : ι → Set α} [Nonempty ι] [Finite ι] (hf : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f) : s ⊆ ⋃ (i : ι), f i ↔ ∃ (i : ι), s ⊆ f i

theorem Set.subset_sUnion_iff_of_directed {α : Type u_2} {S : Set (Set α)} {s : Set α} (hS : S.Nonempty) (hS' : S.Finite) (hS'' : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) S) : s ⊆ sSup S ↔ ∃ t ∈ S, s ⊆ t

Suprema and infima over finite types

We state simplified versions of le_ciSup_if_le and ciSup_mono when the indexing type is finite. This avoids having to explicitly use Finite.bddAbove_range.

Similarly for ciInf.

theorem Finite.le_ciSup_of_le {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] {a : α} {f : ι → α} (c : ι) (h : a ≤ f c) : a ≤ iSup f

theorem Finite.ciInf_le_of_le {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] {a : α} {f : ι → α} (c : ι) (h : f c ≤ a) : iInf f ≤ a

theorem Finite.ciSup_mono {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] {f g : ι → α} (H : ∀ (x : ι), f x ≤ g x) : iSup f ≤ iSup g

theorem Finite.ciInf_mono {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] {f g : ι → α} (H : ∀ (x : ι), f x ≤ g x) : iInf f ≤ iInf g

theorem Finite.le_ciSup {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] (f : ι → α) (i : ι) : f i ≤ ⨆ (j : ι), f j

theorem Finite.ciInf_le {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] (f : ι → α) (i : ι) : ⨅ (j : ι), f j ≤ f i

theorem Finite.ciSup_sup {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} : (⨆ (i : ι), f i) ⊔ a = ⨆ (i : ι), f i ⊔ a

theorem Finite.ciInf_inf {α : Type u_1} {ι : Type u_2} [Finite ι] [ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} : (⨅ (i : ι), f i) ⊓ a = ⨅ (i : ι), f i ⊓ a

theorem Finite.ciSup_prod {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] [ConditionallyCompleteLattice α] (f : ι × ι' → α) : ⨆ (a : ι × ι'), f a = ⨆ (i : ι), ⨆ (i' : ι'), f (i, i')

theorem Finite.ciInf_prod {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] [ConditionallyCompleteLattice α] (f : ι × ι' → α) : ⨅ (a : ι × ι'), f a = ⨅ (i : ι), ⨅ (i' : ι'), f (i, i')

theorem Finite.map_iSup_of_monotoneOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : MonotoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)

theorem Finite.map_iInf_of_monotoneOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : MonotoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨅ (i : ι), f i) = ⨅ (i : ι), g (f i)

theorem Finite.map_iSup_of_antitoneOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : AntitoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨆ (i : ι), f i) = ⨅ (i : ι), g (f i)

theorem Finite.map_iInf_of_antitoneOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : AntitoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨅ (i : ι), f i) = ⨆ (i : ι), g (f i)

theorem Finite.map_iSup_of_monotone {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β} (hg : Monotone g) : g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)

theorem Finite.map_iInf_of_monotone {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β} (hg : Monotone g) : g (⨅ (i : ι), f i) = ⨅ (i : ι), g (f i)

theorem Finite.map_iSup_of_antitone {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β} (hg : Antitone g) : g (⨆ (i : ι), f i) = ⨅ (i : ι), g (f i)

theorem Finite.map_iInf_of_antitone {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β} (hg : Antitone g) : g (⨅ (i : ι), f i) = ⨆ (i : ι), g (f i)