Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2021 Peter Nelson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Peter Nelson, Yaël Dillies
! This file was ported from Lean 3 source module data.fintype.order
! leanprover-community/mathlib commit 1126441d6bccf98c81214a0780c73d499f6721fe
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Lattice
import Mathlib.Data.Finset.Order
/-!
# 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 `CompleteBooleanAlgebra`.
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`
-/
open Finset
namespace Fintype
variable { ι α : Type _ : Type (?u.87189+1)} [ Fintype ι ] [ Fintype α ]
section Nonempty
variable ( α ) [ Nonempty α ]
-- See note [reducible non-instances]
/-- Constructs the `⊥` of a finite nonempty `SemilatticeInf`. -/
@[reducible]
def toOrderBot [ SemilatticeInf α ] : OrderBot : (α : Type ?u.50) → [inst : LE α Type ?u.50 α where
bot := univ . inf' univ_nonempty id : {α : Sort ?u.811} → α → α
bot_le a := inf'_le _ <| mem_univ : ∀ {α : Type ?u.829} [inst : Fintype α x : α ), x ∈ univ a
#align fintype.to_order_bot Fintype.toOrderBot
-- See note [reducible non-instances]
/-- Constructs the `⊤` of a finite nonempty `SemilatticeSup` -/
@[reducible]
def toOrderTop [ SemilatticeSup : Type ?u.1004 → Type ?u.1004 α ] : OrderTop : (α : Type ?u.1007) → [inst : LE α Type ?u.1007 α where
top := univ . sup' univ_nonempty id : {α : Sort ?u.1980} → α → α
-- Porting note: needed to make `id` explicit
le_top a := le_sup' id : {α : Sort ?u.1998} → α → α <| mem_univ : ∀ {α : Type ?u.2004} [inst : Fintype α x : α ), x ∈ univ a
#align fintype.to_order_top Fintype.toOrderTop
-- See note [reducible non-instances]
/-- Constructs the `⊤` and `⊥` of a finite nonempty `Lattice`. -/
@[reducible]
def toBoundedOrder [ Lattice α ] : BoundedOrder : (α : Type ?u.2136) → [inst : LE α Type ?u.2136 α :=
{ toOrderBot α , toOrderTop α with }
#align fintype.to_bounded_order Fintype.toBoundedOrder
end Nonempty
section BoundedOrder
variable ( α )
open Classical
-- See note [reducible non-instances]
/-- A finite bounded lattice is complete. -/
@[reducible]
noncomputable def toCompleteLattice [ Lattice α ] [ BoundedOrder : (α : Type ?u.2936) → [inst : LE α Type ?u.2936 α ] : CompleteLattice : Type ?u.3264 → Type ?u.3264 α :=
{ ‹Lattice α›,
‹BoundedOrder α› with
sSup := fun s => s . toFinset . sup id : {α : Sort ?u.3726} → α → α
sInf := fun s => s . toFinset . inf id : {α : Sort ?u.4165} → α → α
le_sSup := fun _ _ ha => Finset.le_sup (f := id : {α : Sort ?u.3784} → α → α ) ( Set.mem_toFinset . mpr : ∀ {a b : Prop }, (a ↔ b b → a ha )
sSup_le := fun s _ ha => Finset.sup_le fun b hb => ha _ <| Set.mem_toFinset . mp : ∀ {a b : Prop }, (a ↔ b a → b hb
sInf_le := fun _ _ ha => Finset.inf_le ( Set.mem_toFinset . mpr : ∀ {a b : Prop }, (a ↔ b b → a ha )
le_sInf := fun s _ ha => Finset.le_inf fun b hb => ha _ <| Set.mem_toFinset . mp : ∀ {a b : Prop }, (a ↔ b a → b hb }
#align fintype.to_complete_lattice Fintype.toCompleteLattice
-- Porting note: `convert` doesn't work as well as it used to.
-- See note [reducible non-instances]
/-- A finite bounded distributive lattice is completely distributive. -/
@[reducible]
noncomputable def toCompleteDistribLattice [ DistribLattice : Type ?u.5033 → Type ?u.5033 α ] [ BoundedOrder : (α : Type ?u.5036) → [inst : LE α Type ?u.5036 α ] :
CompleteDistribLattice : Type ?u.5420 → Type ?u.5420 α :=
{ toCompleteLattice α with
iInf_sup_le_sup_sInf := fun a s => by
convert ( Finset.inf_sup_distrib_left s . toFinset id : {α : Sort ?u.7837} → α → α a ). ge using 1
rw [ Finset.inf_eq_iInf h.e'_3 (⨅ b , ⨅ h , a ⊔ b ) = ⨅ a_1 , ⨅ h , a ⊔ id a_1 ] h.e'_3 (⨅ b , ⨅ h , a ⊔ b ) = ⨅ a_1 , ⨅ h , a ⊔ id a_1
simp_rw [ h.e'_3 (⨅ b , ⨅ x , a ⊔ b ) = ⨅ a_1 , ⨅ h , a ⊔ id a_1 Set.mem_toFinset h.e'_3 (⨅ b , ⨅ x , a ⊔ b ) = ⨅ a_1 , ⨅ x , a ⊔ id a_1 ] h.e'_3 (⨅ b , ⨅ x , a ⊔ b ) = ⨅ a_1 , ⨅ x , a ⊔ id a_1
rfl
inf_sSup_le_iSup_inf := fun a s => by
convert ( Finset.sup_inf_distrib_left s . toFinset id : {α : Sort ?u.5742} → α → α a ). le using 1
rw [ Finset.sup_eq_iSup h.e'_4 (⨆ b , ⨆ h , a ⊓ b ) = ⨆ a_1 , ⨆ h , a ⊓ id a_1 ] h.e'_4 (⨆ b , ⨆ h , a ⊓ b ) = ⨆ a_1 , ⨆ h , a ⊓ id a_1
simp_rw [ h.e'_4 (⨆ b , ⨆ x , a ⊓ b ) = ⨆ a_1 , ⨆ h , a ⊓ id a_1 Set.mem_toFinset h.e'_4 (⨆ b , ⨆ x , a ⊓ b ) = ⨆ a_1 , ⨆ x , a ⊓ id a_1 ] h.e'_4 (⨆ b , ⨆ x , a ⊓ b ) = ⨆ a_1 , ⨆ x , a ⊓ id a_1
rfl }
#align fintype.to_complete_distrib_lattice Fintype.toCompleteDistribLattice
-- See note [reducible non-instances]
/-- A finite bounded linear order is complete. -/
@[reducible]
noncomputable def toCompleteLinearOrder [ LinearOrder : Type ?u.10332 → Type ?u.10332 α ] [ BoundedOrder : (α : Type ?u.10335) → [inst : LE α Type ?u.10335 α ] : CompleteLinearOrder : Type ?u.10745 → Type ?u.10745 α :=
{ toCompleteLattice α , ‹LinearOrder α› with }
#align fintype.to_complete_linear_order Fintype.toCompleteLinearOrder
-- See note [reducible non-instances]
/-- A finite boolean algebra is complete. -/
@[reducible]
noncomputable def toCompleteBooleanAlgebra [ BooleanAlgebra : Type ?u.87201 → Type ?u.87201 α ] : CompleteBooleanAlgebra : Type ?u.87204 → Type ?u.87204 α :=
-- Porting note: using `Fintype.toCompleteDistribLattice α` caused timeouts
{ Fintype.toCompleteLattice α ,
‹BooleanAlgebra α› with
iInf_sup_le_sup_sInf := fun a s => by
convert ( Finset.inf_sup_distrib_left s . toFinset id : {α : Sort ?u.99423} → α → α a ). ge : ∀ {α : Type ?u.99451} [inst : Preorder α x y : α }, x = y y ≤ x ge using 1
rw [ Finset.inf_eq_iInf h.e'_3 (⨅ b , ⨅ h , a ⊔ b ) = ⨅ a_1 , ⨅ h , a ⊔ id a_1 ] h.e'_3 (⨅ b , ⨅ h , a ⊔ b ) = ⨅ a_1 , ⨅ h , a ⊔ id a_1
simp_rw [ h.e'_3 (⨅ b , ⨅ x , a ⊔ b ) = ⨅ a_1 , ⨅ x , a ⊔ id a_1 Set.mem_toFinset h.e'_3 (⨅ b , ⨅ x , a ⊔ b ) = ⨅ a_1 , ⨅ x , a ⊔ id a_1 ] h.e'_3 (⨅ b , ⨅ x , a ⊔ b ) = ⨅ a_1 , ⨅ x , a ⊔ id a_1
rfl
inf_sSup_le_iSup_inf := fun a s => by
convert ( Finset.sup_inf_distrib_left s . toFinset id : {α : Sort ?u.97442} → α → α a ). le : ∀ {α : Type ?u.97492} [inst : Preorder α a b : α }, a = b a ≤ b le using 1
rw [ Finset.sup_eq_iSup h.e'_4 (⨆ b , ⨆ h , a ⊓ b ) = ⨆ a_1 , ⨆ h , a ⊓ id a_1 ] h.e'_4 (⨆ b , ⨆ h , a ⊓ b ) = ⨆ a_1 , ⨆ h , a ⊓ id a_1
simp_rw [ h.e'_4 (⨆ b , ⨆ x , a ⊓ b ) = ⨆ a_1 , ⨆ x , a ⊓ id a_1 Set.mem_toFinset h.e'_4 (⨆ b , ⨆ x , a ⊓ b ) = ⨆ a_1 , ⨆ x , a ⊓ id a_1 ] h.e'_4 (⨆ b , ⨆ x , a ⊓ b ) = ⨆ a_1 , ⨆ x , a ⊓ id a_1
rfl }
#align fintype.to_complete_boolean_algebra Fintype.toCompleteBooleanAlgebra
end BoundedOrder
section Nonempty
variable ( α ) [ Nonempty α ]
-- See note [reducible non-instances]
/-- 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 `⊤`. -/
@[reducible]
noncomputable def toCompleteLatticeOfNonempty [ Lattice : Type ?u.101266 → Type ?u.101266 α ] : CompleteLattice : Type ?u.101269 → Type ?u.101269 α :=
@ toCompleteLattice _ _ _ <| @ toBoundedOrder α _ ⟨ Classical.arbitrary : (α : Sort ?u.101329) → [h : Nonempty α α α ⟩ _
#align fintype.to_complete_lattice_of_nonempty Fintype.toCompleteLatticeOfNonempty
-- See note [reducible non-instances]
/-- 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
`⊤`. -/
@[reducible]
noncomputable def toCompleteLinearOrderOfNonempty [ LinearOrder : Type ?u.101398 → Type ?u.101398 α ] : CompleteLinearOrder : Type ?u.101401 → Type ?u.101401 α :=
{ toCompleteLatticeOfNonempty α , ‹LinearOrder α› with }
#align fintype.to_complete_linear_order_of_nonempty Fintype.toCompleteLinearOrderOfNonempty
end Nonempty
end Fintype
/-! ### Concrete instances -/
noncomputable instance Fin.completeLinearOrder { n : ℕ } : CompleteLinearOrder : Type ?u.178720 → Type ?u.178720 ( Fin ( n + 1 )) :=
Fintype.toCompleteLinearOrder _
noncomputable instance Bool.completeLinearOrder : CompleteLinearOrder : Type ?u.178921 → Type ?u.178921 Bool :=
Fintype.toCompleteLinearOrder _
noncomputable instance Bool.completeBooleanAlgebra : CompleteBooleanAlgebra : Type ?u.179033 → Type ?u.179033 Bool :=
Fintype.toCompleteBooleanAlgebra _
/-! ### Directed Orders -/
variable { α : Type _ : Type (?u.179088+1)}
theorem Directed.fintype_le { r : α → α → Prop } [ IsTrans α r ] { β γ : Type _ : Type (?u.179105+1)} [ Nonempty γ ] { f : γ → α }
[ Fintype : Type ?u.179118 → Type ?u.179118 β ] ( D : Directed : {α : Type ?u.179122} → {ι : Sort ?u.179121} → (α → α → Prop (ι → α Prop r f ) ( g : β → γ ) : ∃ z , ∀ i , r ( f ( g i )) ( f z ) := by
∃ z , ∀ (i : β ), r (f (g i f z
classical
∃ z , ∀ (i : β ), r (f (g i f z
obtain ⟨z, hz⟩ : ∃ z , ∀ (i : γ ), i ∈ image g univ r (f i f z z ⟨z, hz⟩ : ∃ z , ∀ (i : γ ), i ∈ image g univ r (f i f z hz : ∀ (i : γ ), i ∈ image g univ r (f i f z hz ⟨z, hz⟩ : ∃ z , ∀ (i : γ ), i ∈ image g univ r (f i f z := D . finset_le ( Finset.image g Finset.univ ) intro ∃ z , ∀ (i : β ), r (f (g i f z
∃ z , ∀ (i : β ), r (f (g i f z
exact ⟨ z , fun i => hz : ∀ (i : γ ), i ∈ image g univ r (f i f z hz ( g i ) ( Finset.mem_image_of_mem g ( Finset.mem_univ : ∀ {α : Type ?u.179593} [inst : Fintype α x : α ), x ∈ univ i ))⟩
#align directed.fintype_le Directed.fintype_le
theorem Fintype.exists_le [ Nonempty α ] [ Preorder : Type ?u.179631 → Type ?u.179631 α ] [ IsDirected α (· ≤ ·) ] { β : Type _ : Type (?u.179658+1)} [ Fintype : Type ?u.179661 → Type ?u.179661 β ]
( f : β → α ) : ∃ M , ∀ i , f i ≤ M :=
directed_id . fintype_le : ∀ {α : Type ?u.179712} {r : α → α → Prop inst : IsTrans α r β : Type ?u.179713} {γ : Type ?u.179714}
[inst : Nonempty γ f : γ → α inst : Fintype β Directed r f ∀ (g : β → γ ∃ z , ∀ (i : β ), r (f (g i f z _
#align fintype.exists_le Fintype.exists_le
theorem Fintype.bddAbove_range [ Nonempty α ] [ Preorder : Type ?u.179936 → Type ?u.179936 α ] [ IsDirected α (· ≤ ·) ] { β : Type _ : Type (?u.179963+1)}
[ Fintype : Type ?u.179966 → Type ?u.179966 β ] ( f : β → α ) : BddAbove ( Set.range : {α : Type ?u.179999} → {ι : Sort ?u.179998} → (ι → α Set α f ) := by
obtain ⟨M, hM⟩ : ∃ M , ∀ (i : β ), f i ≤ M M ⟨M, hM⟩ : ∃ M , ∀ (i : β ), f i ≤ M hM ⟨M, hM⟩ : ∃ M , ∀ (i : β ), f i ≤ M := Fintype.exists_le f
refine' ⟨ M , fun a ha => _ ⟩
obtain ⟨ b , rfl ⟩ := ha
exact hM b
#align fintype.bdd_above_range Fintype.bddAbove_range