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) 2018 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
! This file was ported from Lean 3 source module order.conditionally_complete_lattice.basic
! leanprover-community/mathlib commit 29cb56a7b35f72758b05a30490e1f10bd62c35c1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Bounds.Basic
import Mathlib.Order.WellFounded
import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Data.Set.Lattice
/-!
# Theory of conditionally complete lattices.
A conditionally complete lattice is a lattice in which every non-empty bounded subset `s`
has a least upper bound and a greatest lower bound, denoted below by `sSup s` and `sInf s`.
Typical examples are `ℝ`, `ℕ`, and `ℤ` with their usual orders.
The theory is very comparable to the theory of complete lattices, except that suitable
boundedness and nonemptiness assumptions have to be added to most statements.
We introduce two predicates `BddAbove` and `BddBelow` to express this boundedness, prove
their basic properties, and then go on to prove most useful properties of `sSup` and `sInf`
in conditionally complete lattices.
To differentiate the statements between complete lattices and conditionally complete
lattices, we prefix `sInf` and `sSup` in the statements by `c`, giving `csInf` and `csSup`.
For instance, `sInf_le` is a statement in complete lattices ensuring `sInf s ≤ x`,
while `csInf_le` is the same statement in conditionally complete lattices
with an additional assumption that `s` is bounded below.
-/
open Function OrderDual Set
variable { α β γ : Type _ : Type (?u.41916+1)} { ι : Sort _ }
section
/-!
Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α`
-/
open Classical
noncomputable instance { α : Type _ } [ Preorder α ] [ SupSet α ] : SupSet ( WithTop α ) :=
⟨ fun S =>
if ⊤ ∈ S then ⊤ else if BddAbove (( fun ( a : α ) ↦ ↑ a ) ⁻¹' S : Set α ) then
↑( sSup (( fun ( a : α ) ↦ ( a : WithTop α )) ⁻¹' S : Set α )) else ⊤ ⟩
noncomputable instance { α : Type _ } [ InfSet α ] : InfSet ( WithTop α ) :=
⟨ fun S => if S ⊆ { ⊤ } then ⊤ else ↑( sInf (( fun ( a : α ) ↦ ↑ a ) ⁻¹' S : Set α ))⟩
noncomputable instance { α : Type _ } [ SupSet α ] : SupSet ( WithBot α ) :=
⟨(@ instInfSetWithTop α ᵒᵈ _). sInf ⟩
noncomputable instance { α : Type _ } [ Preorder α ] [ InfSet α ] : InfSet ( WithBot α ) :=
⟨(@ instSupSetWithTop α ᵒᵈ _). sSup ⟩
theorem WithTop.sSup_eq [ Preorder α ] [ SupSet α ] { s : Set ( WithTop α )} ( hs : ⊤ ∉ s )
( hs' : BddAbove ( (↑) ⁻¹' s : Set α )) : sSup s = ↑( sSup ( (↑) ⁻¹' s ) : α ) :=
( if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.1263} {t e : α }, (if c then t else e ) = e hs ). trans : ∀ {α : Sort ?u.1271} {a b c : α }, a = b b = c a = c trans $ if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.1294} {t e : α }, (if c then t else e ) = t hs'
#align with_top.Sup_eq WithTop.sSup_eq
theorem WithTop.sInf_eq [ InfSet α ] { s : Set ( WithTop α )} ( hs : ¬ s ⊆ { ⊤ }) :
sInf s = ↑( sInf ( (↑) ⁻¹' s ) : α ) :=
if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.1606} {t e : α }, (if c then t else e ) = e hs
#align with_top.Inf_eq WithTop.sInf_eq
theorem WithBot.sInf_eq [ Preorder α ] [ InfSet α ] { s : Set ( WithBot α )} ( hs : ⊥ ∉ s )
( hs' : BddBelow ( (↑) ⁻¹' s : Set α )) : sInf s = ↑( sInf ( (↑) ⁻¹' s ) : α ) :=
( if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.2029} {t e : α }, (if c then t else e ) = e hs ). trans : ∀ {α : Sort ?u.2037} {a b c : α }, a = b b = c a = c trans $ if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.2066} {t e : α }, (if c then t else e ) = t hs'
#align with_bot.Inf_eq WithBot.sInf_eq
theorem WithBot.sSup_eq [ SupSet α ] { s : Set ( WithBot α )} ( hs : ¬ s ⊆ { ⊥ }) :
sSup s = ↑( sSup ( (↑) ⁻¹' s ) : α ) :=
if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.2415} {t e : α }, (if c then t else e ) = e hs
#align with_bot.Sup_eq WithBot.sSup_eq
@[ simp ]
theorem WithTop.sInf_empty { α : Type _ } [ InfSet α ] : sInf ( ∅ : Set ( WithTop α )) = ⊤ :=
if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.2586} {t e : α }, (if c then t else e ) = t <| Set.empty_subset : ∀ {α : Type ?u.2589} (s : Set α ∅ ⊆ s _
#align with_top.cInf_empty WithTop.sInf_empty
@[ simp ]
theorem WithTop.iInf_empty { α : Type _ } [ IsEmpty ι ] [ InfSet α ] ( f : ι → WithTop α ) :
(⨅ i , f i ) = ⊤ := by rw [ iInf : {α : Type ?u.2797} → [inst : InfSet α {ι : Sort ?u.2796} → (ι → α α , range_eq_empty , WithTop.sInf_empty ]
#align with_top.cinfi_empty WithTop.iInf_empty
theorem WithTop.coe_sInf' [ InfSet α ] { s : Set α } ( hs : s . Nonempty ) :
↑( sInf s ) = ( sInf (( fun ( a : α ) ↦ ↑ a ) '' s ) : WithTop α ) := by
obtain ⟨ x , hx ⟩ := hs
change _ = ite _ _ _ intro ↑(sInf s = if (fun a => ↑a ) '' s ⊆ {⊤ } ⊤ else ↑(sInf ((fun a => ↑a ) ⁻¹' ((fun a => ↑a ) '' s ) )
split_ifs with h
· cases h : (fun a => ↑a ) '' s ⊆ {⊤ } h ( mem_image_of_mem : ∀ {α : Type ?u.3991} {β : Type ?u.3992} (f : α → β x : α } {a : Set α x ∈ a f x ∈ f '' a _ hx )
· rw [ preimage_image_eq ]
exact Option.some_injective : ∀ (α : Type ?u.4083), Injective Option.some _
#align with_top.coe_Inf' WithTop.coe_sInf'
-- Porting note: the mathlib3 proof uses `range_comp` in the opposite direction and
-- does not need `rfl`.
@[ norm_cast ]
theorem WithTop.coe_iInf : ∀ {α : Type u_2} {ι : Sort u_1} [inst : Nonempty ι inst : InfSet α f : ι → α ↑(⨅ i , f i ) = ⨅ i , ↑(f i WithTop.coe_iInf [ Nonempty ι ] [ InfSet α ] ( f : ι → α ) :
↑(⨅ i , f i ) = (⨅ i , f i : WithTop α ) := by
↑(⨅ i , f i ) = ⨅ i , ↑(f i rw [ ↑(⨅ i , f i ) = ⨅ i , ↑(f i iInf : {α : Type ?u.4380} → [inst : InfSet α {ι : Sort ?u.4379} → (ι → α α , ↑(⨅ i , f i ) = ⨅ i , ↑(f i iInf : {α : Type ?u.4432} → [inst : InfSet α {ι : Sort ?u.4431} → (ι → α α , ↑(⨅ i , f i ) = ⨅ i , ↑(f i WithTop.coe_sInf' ( range_nonempty f ), ↑(⨅ i , f i ) = ⨅ i , ↑(f i ← range_comp ] ; ↑(⨅ i , f i ) = ⨅ i , ↑(f i rfl
#align with_top.coe_infi WithTop.coe_iInf : ∀ {α : Type u_2} {ι : Sort u_1} [inst : Nonempty ι inst : InfSet α f : ι → α ↑(⨅ i , f i ) = ⨅ i , ↑(f i
theorem WithTop.coe_sSup' [ Preorder α ] [ SupSet α ] { s : Set α } ( hs : BddAbove s ) :
↑( sSup s ) = ( sSup (( fun ( a : α ) ↦ ↑ a ) '' s ) : WithTop α ) := by
change _ = ite _ _ _
rw [ if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.5263} {t e : α }, (if c then t else e ) = e , preimage_image_eq , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.5311} {t e : α }, (if c then t else e ) = t hs ]
· exact Option.some_injective : ∀ (α : Type ?u.5324), Injective Option.some _
· rintro ⟨x, _, ⟨⟩⟩ : ⊤ ∈ (fun a => ↑a ) '' s x ⟨x, _, ⟨⟩⟩ : ⊤ ∈ (fun a => ↑a ) '' s _ ⟨x, _, ⟨⟩⟩ : ⊤ ∈ (fun a => ↑a ) '' s ⟨⟩ ⟨x, _, ⟨⟩⟩ : ⊤ ∈ (fun a => ↑a ) '' s
#align with_top.coe_Sup' WithTop.coe_sSup'
-- Porting note: the mathlib3 proof uses `range_comp` in the opposite direction and
-- does not need `rfl`.
@[ norm_cast ]
theorem WithTop.coe_iSup [ Preorder α ] [ SupSet α ] ( f : ι → α ) ( h : BddAbove ( Set.range : {α : Type ?u.5486} → {ι : Sort ?u.5485} → (ι → α Set α f )) :
↑(⨆ i , f i ) = (⨆ i , f i : WithTop α ) := by
↑(⨆ i , f i ) = ⨆ i , ↑(f i rw [ ↑(⨆ i , f i ) = ⨆ i , ↑(f i iSup : {α : Type ?u.5761} → [inst : SupSet α {ι : Sort ?u.5760} → (ι → α α , ↑(⨆ i , f i ) = ⨆ i , ↑(f i iSup : {α : Type ?u.5817} → [inst : SupSet α {ι : Sort ?u.5816} → (ι → α α , ↑(⨆ i , f i ) = ⨆ i , ↑(f i WithTop.coe_sSup' h , ↑(⨆ i , f i ) = ⨆ i , ↑(f i ← range_comp ] ; ↑(⨆ i , f i ) = ⨆ i , ↑(f i rfl
#align with_top.coe_supr WithTop.coe_iSup
@[ simp ]
theorem WithBot.csSup_empty { α : Type _ } [ SupSet α ] : sSup ( ∅ : Set ( WithBot α )) = ⊥ :=
if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.6164} {t e : α }, (if c then t else e ) = t <| Set.empty_subset : ∀ {α : Type ?u.6167} (s : Set α ∅ ⊆ s _
#align with_bot.cSup_empty WithBot.csSup_empty
@[ simp ]
theorem WithBot.ciSup_empty { α : Type _ } [ IsEmpty ι ] [ SupSet α ] ( f : ι → WithBot α ) :
(⨆ i , f i ) = ⊥ :=
@ WithTop.iInf_empty _ α ᵒᵈ _ _ _
#align with_bot.csupr_empty WithBot.ciSup_empty
@[ norm_cast ]
theorem WithBot.coe_sSup' [ SupSet α ] { s : Set α } ( hs : s . Nonempty ) :
↑( sSup s ) = ( sSup (( fun ( a : α ) ↦ ↑ a ) '' s ) : WithBot α ) :=
@ WithTop.coe_sInf' α ᵒᵈ _ _ hs
#align with_bot.coe_Sup' WithBot.coe_sSup'
@[ norm_cast ]
theorem WithBot.coe_iSup : ∀ [inst : Nonempty ι inst : SupSet α f : ι → α ↑(⨆ i , f i ) = ⨆ i , ↑(f i WithBot.coe_iSup [ Nonempty ι ] [ SupSet α ] ( f : ι → α ) :
↑(⨆ i , f i ) = (⨆ i , f i : WithBot α ) :=
@ WithTop.coe_iInf : ∀ {α : Type ?u.7090} {ι : Sort ?u.7089} [inst : Nonempty ι inst : InfSet α f : ι → α ↑(⨅ i , f i ) = ⨅ i , ↑(f i α ᵒᵈ _ _ _ _
#align with_bot.coe_supr WithBot.coe_iSup : ∀ {α : Type u_2} {ι : Sort u_1} [inst : Nonempty ι inst : SupSet α f : ι → α ↑(⨆ i , f i ) = ⨆ i , ↑(f i
@[ norm_cast ]
theorem WithBot.coe_sInf' [ Preorder α ] [ InfSet α ] { s : Set α } ( hs : BddBelow s ) :
↑( sInf s ) = ( sInf (( fun ( a : α ) ↦ ↑ a ) '' s ) : WithBot α ) :=
@ WithTop.coe_sSup' α ᵒᵈ _ _ _ hs
#align with_bot.coe_Inf' WithBot.coe_sInf'
@[ norm_cast ]
theorem WithBot.coe_iInf [ Preorder α ] [ InfSet α ] ( f : ι → α ) ( h : BddBelow ( Set.range : {α : Type ?u.7826} → {ι : Sort ?u.7825} → (ι → α Set α f )) :
↑(⨅ i , f i ) = (⨅ i , f i : WithBot α ) :=
@ WithTop.coe_iSup α ᵒᵈ _ _ _ _ h
#align with_bot.coe_infi WithBot.coe_iInf
end
/-- A conditionally complete lattice is a lattice in which
every nonempty subset which is bounded above has a supremum, and
every nonempty subset which is bounded below has an infimum.
Typical examples are real numbers or natural numbers.
To differentiate the statements from the corresponding statements in (unconditional)
complete lattices, we prefix sInf and subₛ by a c everywhere. The same statements should
hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness.-/
class ConditionallyCompleteLattice ( α : Type _ ) extends Lattice α , SupSet α , InfSet α where
/-- `a ≤ sSup s` for all `a ∈ s`. -/
le_csSup : ∀ s a , BddAbove s → a ∈ s → a ≤ sSup s
/-- `sSup s ≤ a` for all `a ∈ upperBounds s`. -/
csSup_le : ∀ s a , Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ a
/-- `sInf s ≤ a` for all `a ∈ s`. -/
csInf_le : ∀ s a , BddBelow s → a ∈ s → sInf s ≤ a
/-- `a ≤ sInf s` for all `a ∈ lowerBounds s`. -/
le_csInf : ∀ s a , Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf s
#align conditionally_complete_lattice ConditionallyCompleteLattice : Type u_1 → Type u_1
-- Porting note: mathlib3 used `renaming`
/-- A conditionally complete linear order is a linear order in which
every nonempty subset which is bounded above has a supremum, and
every nonempty subset which is bounded below has an infimum.
Typical examples are real numbers or natural numbers.
To differentiate the statements from the corresponding statements in (unconditional)
complete linear orders, we prefix sInf and sSup by a c everywhere. The same statements should
hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness.-/
class ConditionallyCompleteLinearOrder ( α : Type _ ) extends ConditionallyCompleteLattice : Type ?u.8833 → Type ?u.8833 α where
/-- A `ConditionallyCompleteLinearOrder` is total. -/
le_total ( a b : α ) : a ≤ b ∨ b ≤ a
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
decidableLE : DecidableRel : {α : Sort ?u.8922} → (α → α → Prop Sort (max1?u.8922) (. ≤ . : α → α → Prop )
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
decidableEq : DecidableEq : Sort ?u.8948 → Sort (max1?u.8948) α := @ decidableEqOfDecidableLE _ _ decidableLE
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
decidableLT : DecidableRel : {α : Sort ?u.9001} → (α → α → Prop Sort (max1?u.9001) (. < . : α → α → Prop ) :=
@ decidableLTOfDecidableLE _ _ decidableLE
#align conditionally_complete_linear_order ConditionallyCompleteLinearOrder : Type u_1 → Type u_1
instance ( α : Type _ ) [ ConditionallyCompleteLinearOrder : Type ?u.9860 → Type ?u.9860 α ] : LinearOrder : Type ?u.9863 → Type ?u.9863 α :=
{ ‹ConditionallyCompleteLinearOrder α› with
max := Sup.sup : {α : Type ?u.9938} → [self : Sup α α → α → α , min := Inf.inf : {α : Type ?u.9892} → [self : Inf α α → α → α ,
min_def := fun a b ↦ by
min a b = if a ≤ b a else b by_cases hab : a = b pos min a b = if a ≤ b a else b neg min a b = if a ≤ b a else b
min a b = if a ≤ b a else b · pos min a b = if a ≤ b a else b pos min a b = if a ≤ b a else b neg min a b = if a ≤ b a else b simp [ hab ]
min a b = if a ≤ b a else b · neg min a b = if a ≤ b a else b neg min a b = if a ≤ b a else b rcases ConditionallyCompleteLinearOrder.le_total a b with ( h₁ | h₂ ) neg.inl min a b = if a ≤ b a else b neg.inr min a b = if a ≤ b a else b
neg min a b = if a ≤ b a else b · neg.inl min a b = if a ≤ b a else b neg.inl min a b = if a ≤ b a else b neg.inr min a b = if a ≤ b a else b simp [ h₁ ]
neg min a b = if a ≤ b a else b · neg.inr min a b = if a ≤ b a else b neg.inr min a b = if a ≤ b a else b simp [ show ¬( a ≤ b ) from fun h => hab ( le_antisymm h h₂ ), h₂ ]
max_def := fun a b ↦ by
max a b = if a ≤ b b else a by_cases hab : a = b pos max a b = if a ≤ b b else a neg max a b = if a ≤ b b else a
max a b = if a ≤ b b else a · pos max a b = if a ≤ b b else a pos max a b = if a ≤ b b else a neg max a b = if a ≤ b b else a simp [ hab ]
max a b = if a ≤ b b else a · neg max a b = if a ≤ b b else a neg max a b = if a ≤ b b else a rcases ConditionallyCompleteLinearOrder.le_total a b with ( h₁ | h₂ ) neg.inl max a b = if a ≤ b b else a neg.inr max a b = if a ≤ b b else a
neg max a b = if a ≤ b b else a · neg.inl max a b = if a ≤ b b else a neg.inl max a b = if a ≤ b b else a neg.inr max a b = if a ≤ b b else a simp [ h₁ ]
neg max a b = if a ≤ b b else a · neg.inr max a b = if a ≤ b b else a neg.inr max a b = if a ≤ b b else a simp [ show ¬( a ≤ b ) from fun h => hab ( le_antisymm h h₂ ), h₂ ] }
/-- A conditionally complete linear order with `Bot` is a linear order with least element, in which
every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily
bounded below) has an infimum. A typical example is the natural numbers.
To differentiate the statements from the corresponding statements in (unconditional)
complete linear orders, we prefix `sInf` and `sSup` by a c everywhere. The same statements should
hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness.-/
class ConditionallyCompleteLinearOrderBot ( α : Type _ : Type (?u.12582+1)) extends ConditionallyCompleteLinearOrder : Type ?u.12587 → Type ?u.12587 α ,
Bot α where
/-- `⊥` is the least element -/
bot_le : ∀ x : α , ⊥ ≤ x
/-- The supremum of the empty set is `⊥` -/
csSup_empty : sSup ∅ = ⊥
#align conditionally_complete_linear_order_bot ConditionallyCompleteLinearOrderBot : Type u_1 → Type u_1
-- see Note [lower instance priority]
instance ( priority := 100) ConditionallyCompleteLinearOrderBot.toOrderBot
[ h : ConditionallyCompleteLinearOrderBot : Type ?u.12918 → Type ?u.12918 α ] : OrderBot : (α : Type ?u.12921) → [inst : LE α Type ?u.12921 α :=
{ h with }
#align conditionally_complete_linear_order_bot.to_order_bot ConditionallyCompleteLinearOrderBot.toOrderBot
-- see Note [lower instance priority]
/-- A complete lattice is a conditionally complete lattice, as there are no restrictions
on the properties of sInf and sSup in a complete lattice.-/
instance ( priority := 100) CompleteLattice.toConditionallyCompleteLattice [ CompleteLattice : Type ?u.13165 → Type ?u.13165 α ] :
ConditionallyCompleteLattice : Type ?u.13168 → Type ?u.13168 α :=
{ ‹CompleteLattice α› with
le_csSup := by intros ; apply le_sSup ; assumption
csSup_le := by intros ; apply sSup_le a ∀ (b : α ), b ∈ s✝ b ≤ a✝² ; a ∀ (b : α ), b ∈ s✝ b ≤ a✝² assumption
csInf_le := by intros ; apply sInf_le ; assumption
le_csInf := by intros ; apply le_sInf a ∀ (b : α ), b ∈ s✝ a✝² ≤ b ; a ∀ (b : α ), b ∈ s✝ a✝² ≤ b assumption }
#align complete_lattice.to_conditionally_complete_lattice CompleteLattice.toConditionallyCompleteLattice
-- see Note [lower instance priority]
instance ( priority := 100) CompleteLinearOrder.toConditionallyCompleteLinearOrderBot { α : Type _ : Type (?u.13465+1)}
[ h : CompleteLinearOrder : Type ?u.13468 → Type ?u.13468 α ] : ConditionallyCompleteLinearOrderBot : Type ?u.13471 → Type ?u.13471 α :=
{ CompleteLattice.toConditionallyCompleteLattice , h with csSup_empty := sSup_empty }
#align complete_linear_order.to_conditionally_complete_linear_order_bot CompleteLinearOrder.toConditionallyCompleteLinearOrderBot
section
open Classical
/-- A well founded linear order is conditionally complete, with a bottom element. -/
@[reducible]
noncomputable def IsWellOrder.conditionallyCompleteLinearOrderBot ( α : Type _ : Type (?u.13816+1))
[ i₁ : _root_.LinearOrder : Type ?u.13819 → Type ?u.13819 α ] [ i₂ : OrderBot : (α : Type ?u.13822) → [inst : LE α Type ?u.13822 α ] [ h : IsWellOrder α (· < ·) ] :
ConditionallyCompleteLinearOrderBot : Type ?u.14135 → Type ?u.14135 α :=
{ i₁ , i₂ , LinearOrder.toLattice with
sInf := fun s => if hs : s . Nonempty then h . wf . min s hs else ⊥
csInf_le := fun s a _ has => by
have s_ne : s . Nonempty := ⟨ a , has ⟩
simpa [ s_ne ] using not_lt . 1 : ∀ {a b : Prop }, (a ↔ b a → b ( h . wf . not_lt_min s s_ne has )
le_csInf := fun s a hs has => by
simp only [ hs , dif_pos ]
exact has ( h . wf . min_mem s hs )
sSup := fun s => if hs : ( upperBounds s ). Nonempty then h . wf . min _ hs else ⊥
le_csSup := fun s a hs has => by
have h's : ( upperBounds s ). Nonempty := hs
simp only [ h's , dif_pos ]
exact h . wf . min_mem _ h's has
csSup_le := fun s a _ has => by
have h's : ( upperBounds s ). Nonempty := ⟨ a , has ⟩
simp only [ h's , dif_pos ]
simpa using h . wf . not_lt_min _ h's has
csSup_empty := by simpa using eq_bot_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( not_lt . 1 : ∀ {a b : Prop }, (a ↔ b a → b <| h . wf . not_lt_min _ _ <| mem_univ : ∀ {α : Type ?u.21294} (x : α ), x ∈ univ ⊥ ) }
#align is_well_order.conditionally_complete_linear_order_bot IsWellOrder.conditionallyCompleteLinearOrderBot
end
section OrderDual
instance ( α : Type _ : Type (?u.21975+1)) [ ConditionallyCompleteLattice : Type ?u.21978 → Type ?u.21978 α ] : ConditionallyCompleteLattice : Type ?u.21981 → Type ?u.21981 α ᵒᵈ :=
{ instInfOrderDual : (α : Type ?u.21988) → [inst : Sup α Inf α ᵒᵈ α , instSupOrderDual : (α : Type ?u.22019) → [inst : Inf α Sup α ᵒᵈ α , OrderDual.lattice α with
le_csSup := @ ConditionallyCompleteLattice.csInf_le α _
csSup_le := @ ConditionallyCompleteLattice.le_csInf α _
le_csInf := @ ConditionallyCompleteLattice.csSup_le α _
csInf_le := @ ConditionallyCompleteLattice.le_csSup α _ }
instance ( α : Type _ : Type (?u.22302+1)) [ ConditionallyCompleteLinearOrder : Type ?u.22305 → Type ?u.22305 α ] : ConditionallyCompleteLinearOrder : Type ?u.22308 → Type ?u.22308 α ᵒᵈ :=
{ instConditionallyCompleteLatticeOrderDual α , OrderDual.linearOrder α with }
end OrderDual
/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sup` function
that returns the least upper bound of a nonempty set which is bounded above. Usually this
constructor provides poor definitional equalities. If other fields are known explicitly, they
should be provided; for example, if `inf` is known explicitly, construct the
`ConditionallyCompleteLattice` instance as
```
instance : ConditionallyCompleteLattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, sInf
..conditionallyCompleteLatticeOfsSup my_T _ }
```
-/
def conditionallyCompleteLatticeOfsSup ( α : Type _ : Type (?u.22697+1)) [ H1 : PartialOrder : Type ?u.22700 → Type ?u.22700 α ] [ H2 : SupSet α ]
( bddAbove_pair : ∀ (a b : α ), BddAbove {a , b } bddAbove_pair : ∀ a b : α , BddAbove ({ a , b } : Set α ))
( bddBelow_pair : ∀ (a b : α ), BddBelow {a , b } bddBelow_pair : ∀ a b : α , BddBelow ({ a , b } : Set α ))
( isLUB_sSup : ∀ s : Set α , BddAbove s → s . Nonempty → IsLUB s ( sSup s )) :
ConditionallyCompleteLattice : Type ?u.22930 → Type ?u.22930 α :=
{ H1 , H2 with
sup := fun a b => sSup { a , b }
le_sup_left := fun a b =>
( isLUB_sSup { a , b } ( bddAbove_pair : ∀ (a b : α ), BddAbove {a , b } bddAbove_pair a b ) ( insert_nonempty _ _ )). 1 : ∀ {a b : Prop }, a ∧ b a ( mem_insert _ _ )
le_sup_right := fun a b =>
( isLUB_sSup { a , b } ( bddAbove_pair : ∀ (a b : α ), BddAbove {a , b } bddAbove_pair a b ) ( insert_nonempty _ _ )). 1 : ∀ {a b : Prop }, a ∧ b a
( mem_insert_of_mem : ∀ {α : Type ?u.23158} {x : α } {s : Set α y : α ), x ∈ s x ∈ insert y s _ ( mem_singleton : ∀ {α : Type ?u.23163} (a : α ), a ∈ {a } _ ))
sup_le := fun a b _ hac hbc =>
( isLUB_sSup { a , b } ( bddAbove_pair : ∀ (a b : α ), BddAbove {a , b } bddAbove_pair a b ) (