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 Cmdinstead of Ctrl.
```/-
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 ?u.83856α β: Type ?u.17β γ: Type ?u.20γ : Type _: Type (?u.41916+1)Type _} {ι: Sort ?u.85427ι : Sort _: Type ?u.11SortSort _: Type ?u.11 _}

section

/-!
Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α`
-/

open Classical

noncomputable instance: {α : Type u_1} → [inst : Preorder α] → [inst : SupSet α] → SupSet (WithTop α)instance {α: Type ?u.26α : Type _: Type (?u.26+1)Type _} [Preorder: Type ?u.29 → Type ?u.29Preorder α: Type ?u.26α] [SupSet: Type ?u.32 → Type ?u.32SupSet α: Type ?u.26α] : SupSet: Type ?u.35 → Type ?u.35SupSet (WithTop: Type ?u.36 → Type ?u.36WithTop α: Type ?u.26α) :=
⟨fun S: ?m.47S =>
if ⊤: ?m.55⊤ ∈ S: ?m.47S then ⊤: ?m.106⊤ else if BddAbove: {α : Type ?u.133} → [inst : Preorder α] → Set α → PropBddAbove ((fun (a: αa : α: Type ?u.26α) ↦ ↑a: αa) ⁻¹' S: ?m.47S : Set: Type ?u.137 → Type ?u.137Set α: Type ?u.26α) then
↑(sSup: {α : Type ?u.164} → [self : SupSet α] → Set α → αsSup ((fun (a: αa : α: Type ?u.26α) ↦ (a: αa : WithTop: Type ?u.177 → Type ?u.177WithTop α: Type ?u.26α)) ⁻¹' S: ?m.47S : Set: Type ?u.168 → Type ?u.168Set α: Type ?u.26α)) else ⊤: ?m.318⊤⟩

noncomputable instance: {α : Type u_1} → [inst : InfSet α] → InfSet (WithTop α)instance {α: Type ?u.440α : Type _: Type (?u.440+1)Type _} [InfSet: Type ?u.443 → Type ?u.443InfSet α: Type ?u.440α] : InfSet: Type ?u.446 → Type ?u.446InfSet (WithTop: Type ?u.447 → Type ?u.447WithTop α: Type ?u.440α) :=
⟨fun S: ?m.457S => if S: ?m.457S ⊆ {⊤: ?m.476⊤} then ⊤: ?m.532⊤ else ↑(sInf: {α : Type ?u.559} → [self : InfSet α] → Set α → αsInf ((fun (a: αa : α: Type ?u.440α) ↦ ↑a: αa) ⁻¹' S: ?m.457S : Set: Type ?u.563 → Type ?u.563Set α: Type ?u.440α))⟩

noncomputable instance: {α : Type u_1} → [inst : SupSet α] → SupSet (WithBot α)instance {α: Type ?u.757α : Type _: Type (?u.757+1)Type _} [SupSet: Type ?u.760 → Type ?u.760SupSet α: Type ?u.757α] : SupSet: Type ?u.763 → Type ?u.763SupSet (WithBot: Type ?u.764 → Type ?u.764WithBot α: Type ?u.757α) :=
⟨(@instInfSetWithTop: {α : Type ?u.773} → [inst : InfSet α] → InfSet (WithTop α)instInfSetWithTop α: Type ?u.757αᵒᵈ _).sInf: {α : Type ?u.790} → [self : InfSet α] → Set α → αsInf⟩

noncomputable instance: {α : Type u_1} → [inst : Preorder α] → [inst : InfSet α] → InfSet (WithBot α)instance {α: Type ?u.824α : Type _: Type (?u.824+1)Type _} [Preorder: Type ?u.827 → Type ?u.827Preorder α: Type ?u.824α] [InfSet: Type ?u.830 → Type ?u.830InfSet α: Type ?u.824α] : InfSet: Type ?u.833 → Type ?u.833InfSet (WithBot: Type ?u.834 → Type ?u.834WithBot α: Type ?u.824α) :=
⟨(@instSupSetWithTop: {α : Type ?u.844} → [inst : Preorder α] → [inst : SupSet α] → SupSet (WithTop α)instSupSetWithTop α: Type ?u.824αᵒᵈ _).sSup: {α : Type ?u.870} → [self : SupSet α] → Set α → αsSup⟩

theorem WithTop.sSup_eq: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SupSet α] {s : Set (WithTop α)},
¬⊤ ∈ s → BddAbove (some ⁻¹' s) → sSup s = ↑(sSup (some ⁻¹' s))WithTop.sSup_eq [Preorder: Type ?u.910 → Type ?u.910Preorder α: Type ?u.898α] [SupSet: Type ?u.913 → Type ?u.913SupSet α: Type ?u.898α] {s: Set (WithTop α)s : Set: Type ?u.916 → Type ?u.916Set (WithTop: Type ?u.917 → Type ?u.917WithTop α: Type ?u.898α)} (hs: ¬⊤ ∈ shs : ⊤: ?m.926⊤ ∉ s: Set (WithTop α)s)
(hs': BddAbove (?m.994 ⁻¹' s)hs' : BddAbove: {α : Type ?u.970} → [inst : Preorder α] → Set α → PropBddAbove ((↑): α → WithTop α(↑) ⁻¹' s: Set (WithTop α)s : Set: Type ?u.987 → Type ?u.987Set α: Type ?u.898α)) : sSup: {α : Type ?u.1005} → [self : SupSet α] → Set α → αsSup s: Set (WithTop α)s = ↑(sSup: {α : Type ?u.1032} → [self : SupSet α] → Set α → αsSup ((↑): α → WithTop α(↑) ⁻¹' s: Set (WithTop α)s) : α: Type ?u.898α) :=
(if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1263} {t e : α}, (if c then t else e) = eif_neg hs: ¬⊤ ∈ shs).trans: ∀ {α : Sort ?u.1271} {a b c : α}, a = b → b = c → a = ctrans \$ if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1294} {t e : α}, (if c then t else e) = tif_pos hs': BddAbove (some ⁻¹' s)hs'
#align with_top.Sup_eq WithTop.sSup_eq: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SupSet α] {s : Set (WithTop α)},
¬⊤ ∈ s → BddAbove (WithTop.some ⁻¹' s) → sSup s = ↑(sSup (WithTop.some ⁻¹' s))WithTop.sSup_eq

theorem WithTop.sInf_eq: ∀ [inst : InfSet α] {s : Set (WithTop α)}, ¬s ⊆ {⊤} → sInf s = ↑(sInf (some ⁻¹' s))WithTop.sInf_eq [InfSet: Type ?u.1334 → Type ?u.1334InfSet α: Type ?u.1322α] {s: Set (WithTop α)s : Set: Type ?u.1337 → Type ?u.1337Set (WithTop: Type ?u.1338 → Type ?u.1338WithTop α: Type ?u.1322α)} (hs: ¬s ⊆ {⊤}hs : ¬s: Set (WithTop α)s ⊆ {⊤: ?m.1359⊤}) :
sInf: {α : Type ?u.1408} → [self : InfSet α] → Set α → αsInf s: Set (WithTop α)s = ↑(sInf: {α : Type ?u.1432} → [self : InfSet α] → Set α → αsInf ((↑): α → WithTop α(↑) ⁻¹' s: Set (WithTop α)s) : α: Type ?u.1322α) :=
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1606} {t e : α}, (if c then t else e) = eif_neg hs: ¬s ⊆ {⊤}hs
#align with_top.Inf_eq WithTop.sInf_eq: ∀ {α : Type u_1} [inst : InfSet α] {s : Set (WithTop α)}, ¬s ⊆ {⊤} → sInf s = ↑(sInf (WithTop.some ⁻¹' s))WithTop.sInf_eq

theorem WithBot.sInf_eq: ∀ [inst : Preorder α] [inst_1 : InfSet α] {s : Set (WithBot α)},
¬⊥ ∈ s → BddBelow (some ⁻¹' s) → sInf s = ↑(sInf (some ⁻¹' s))WithBot.sInf_eq [Preorder: Type ?u.1651 → Type ?u.1651Preorder α: Type ?u.1639α] [InfSet: Type ?u.1654 → Type ?u.1654InfSet α: Type ?u.1639α] {s: Set (WithBot α)s : Set: Type ?u.1657 → Type ?u.1657Set (WithBot: Type ?u.1658 → Type ?u.1658WithBot α: Type ?u.1639α)} (hs: ¬⊥ ∈ shs : ⊥: ?m.1667⊥ ∉ s: Set (WithBot α)s)
(hs': BddBelow (some ⁻¹' s)hs' : BddBelow: {α : Type ?u.1719} → [inst : Preorder α] → Set α → PropBddBelow ((↑): α → WithBot α(↑) ⁻¹' s: Set (WithBot α)s : Set: Type ?u.1736 → Type ?u.1736Set α: Type ?u.1639α)) : sInf: {α : Type ?u.1754} → [self : InfSet α] → Set α → αsInf s: Set (WithBot α)s = ↑(sInf: {α : Type ?u.1781} → [self : InfSet α] → Set α → αsInf ((↑): α → WithBot α(↑) ⁻¹' s: Set (WithBot α)s) : α: Type ?u.1639α) :=
(if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.2029} {t e : α}, (if c then t else e) = eif_neg hs: ¬⊥ ∈ shs).trans: ∀ {α : Sort ?u.2037} {a b c : α}, a = b → b = c → a = ctrans \$ if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.2066} {t e : α}, (if c then t else e) = tif_pos hs': BddBelow (some ⁻¹' s)hs'
#align with_bot.Inf_eq WithBot.sInf_eq: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : InfSet α] {s : Set (WithBot α)},
¬⊥ ∈ s → BddBelow (WithBot.some ⁻¹' s) → sInf s = ↑(sInf (WithBot.some ⁻¹' s))WithBot.sInf_eq

theorem WithBot.sSup_eq: ∀ {α : Type u_1} [inst : SupSet α] {s : Set (WithBot α)}, ¬s ⊆ {⊥} → sSup s = ↑(sSup (some ⁻¹' s))WithBot.sSup_eq [SupSet: Type ?u.2122 → Type ?u.2122SupSet α: Type ?u.2110α] {s: Set (WithBot α)s : Set: Type ?u.2125 → Type ?u.2125Set (WithBot: Type ?u.2126 → Type ?u.2126WithBot α: Type ?u.2110α)} (hs: ¬s ⊆ {⊥}hs : ¬s: Set (WithBot α)s ⊆ {⊥: ?m.2147⊥}) :
sSup: {α : Type ?u.2204} → [self : SupSet α] → Set α → αsSup s: Set (WithBot α)s = ↑(sSup: {α : Type ?u.2228} → [self : SupSet α] → Set α → αsSup ((↑): α → WithBot α(↑) ⁻¹' s: Set (WithBot α)s) : α: Type ?u.2110α) :=
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.2415} {t e : α}, (if c then t else e) = eif_neg hs: ¬s ⊆ {⊥}hs
#align with_bot.Sup_eq WithBot.sSup_eq: ∀ {α : Type u_1} [inst : SupSet α] {s : Set (WithBot α)}, ¬s ⊆ {⊥} → sSup s = ↑(sSup (WithBot.some ⁻¹' s))WithBot.sSup_eq

@[simp]
theorem WithTop.sInf_empty: ∀ {α : Type u_1} [inst : InfSet α], sInf ∅ = ⊤WithTop.sInf_empty {α: Type u_1α : Type _: Type (?u.2471+1)Type _} [InfSet: Type ?u.2474 → Type ?u.2474InfSet α: Type ?u.2471α] : sInf: {α : Type ?u.2478} → [self : InfSet α] → Set α → αsInf (∅: ?m.2485∅ : Set: Type ?u.2482 → Type ?u.2482Set (WithTop: Type ?u.2483 → Type ?u.2483WithTop α: Type ?u.2471α)) = ⊤: ?m.2543⊤ :=
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.2586} {t e : α}, (if c then t else e) = tif_pos <| Set.empty_subset: ∀ {α : Type ?u.2589} (s : Set α), ∅ ⊆ sSet.empty_subset _: Set ?m.2590_
#align with_top.cInf_empty WithTop.sInf_empty: ∀ {α : Type u_1} [inst : InfSet α], sInf ∅ = ⊤WithTop.sInf_empty

@[simp]
theorem WithTop.iInf_empty: ∀ {α : Type u_1} [inst : IsEmpty ι] [inst : InfSet α] (f : ι → WithTop α), (⨅ i, f i) = ⊤WithTop.iInf_empty {α: Type u_1α : Type _: Type (?u.2641+1)Type _} [IsEmpty: Sort ?u.2644 → PropIsEmpty ι: Sort ?u.2638ι] [InfSet: Type ?u.2647 → Type ?u.2647InfSet α: Type ?u.2641α] (f: ι → WithTop αf : ι: Sort ?u.2638ι → WithTop: Type ?u.2652 → Type ?u.2652WithTop α: Type ?u.2641α) :
(⨅ i: ?m.2663i, f: ι → WithTop αf i: ?m.2663i) = ⊤: ?m.2683⊤ := byGoals accomplished! 🐙 α✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop α(⨅ i, f i) = ⊤rw [α✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop α(⨅ i, f i) = ⊤iInf: {α : Type ?u.2797} → [inst : InfSet α] → {ι : Sort ?u.2796} → (ι → α) → αiInf,α✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop αsInf (range fun i => f i) = ⊤ α✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop α(⨅ i, f i) = ⊤range_eq_empty: ∀ {α : Type ?u.2799} {ι : Sort ?u.2798} [inst : IsEmpty ι] (f : ι → α), range f = ∅range_eq_empty,α✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop αsInf ∅ = ⊤ α✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop α(⨅ i, f i) = ⊤WithTop.sInf_empty: ∀ {α : Type ?u.2866} [inst : InfSet α], sInf ∅ = ⊤WithTop.sInf_emptyα✝: Type ?u.2629β: Type ?u.2632γ: Type ?u.2635ι: Sort u_2α: Type u_1inst✝¹: IsEmpty ιinst✝: InfSet αf: ι → WithTop α⊤ = ⊤]Goals accomplished! 🐙
#align with_top.cinfi_empty WithTop.iInf_empty: ∀ {ι : Sort u_2} {α : Type u_1} [inst : IsEmpty ι] [inst : InfSet α] (f : ι → WithTop α), (⨅ i, f i) = ⊤WithTop.iInf_empty

theorem WithTop.coe_sInf': ∀ [inst : InfSet α] {s : Set α}, Set.Nonempty s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)WithTop.coe_sInf' [InfSet: Type ?u.2957 → Type ?u.2957InfSet α: Type ?u.2945α] {s: Set αs : Set: Type ?u.2960 → Type ?u.2960Set α: Type ?u.2945α} (hs: Set.Nonempty shs : s: Set αs.Nonempty: {α : Type ?u.2963} → Set α → PropNonempty) :
↑(sInf: {α : Type ?u.3092} → [self : InfSet α] → Set α → αsInf s: Set αs) = (sInf: {α : Type ?u.2976} → [self : InfSet α] → Set α → αsInf ((fun (a: αa : α: Type ?u.2945α) ↦ ↑a: αa) '' s: Set αs) : WithTop: Type ?u.2975 → Type ?u.2975WithTop α: Type ?u.2945α) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αhs: Set.Nonempty s↑(sInf s) = sInf ((fun a => ↑a) '' s)obtain ⟨x, hx⟩: Set.Nonempty s⟨x: αx⟨x, hx⟩: Set.Nonempty s, hx: x ∈ shx⟨x, hx⟩: Set.Nonempty s⟩ := hs: Set.Nonempty shsα: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sintro↑(sInf s) = sInf ((fun a => ↑a) '' s)
α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αhs: Set.Nonempty s↑(sInf s) = sInf ((fun a => ↑a) '' s)change _: ?m.3191_ = ite: {α : Sort ?u.3193} → (c : Prop) → [h : Decidable c] → α → α → αite _: Prop_ _: ?m.3194_ _: ?m.3194_α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sintro↑(sInf s) = if (fun a => ↑a) '' s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))
α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αhs: Set.Nonempty s↑(sInf s) = sInf ((fun a => ↑a) '' s)split_ifs with hα: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: (fun a => ↑a) '' s ⊆ {⊤}intro.inl↑(sInf s) = ⊤α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))
α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αhs: Set.Nonempty s↑(sInf s) = sInf ((fun a => ↑a) '' s)·α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: (fun a => ↑a) '' s ⊆ {⊤}intro.inl↑(sInf s) = ⊤ α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: (fun a => ↑a) '' s ⊆ {⊤}intro.inl↑(sInf s) = ⊤α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))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 '' amem_image_of_mem _: ?m.3993 → ?m.3994_ hx: x ∈ shx)Goals accomplished! 🐙
α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αhs: Set.Nonempty s↑(sInf s) = sInf ((fun a => ↑a) '' s)·α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))rw [α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))preimage_image_eq: ∀ {α : Type ?u.4064} {β : Type ?u.4065} {f : α → β} (s : Set α), Injective f → f ⁻¹' (f '' s) = spreimage_image_eqα: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf s)α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr.hInjective fun a => ↑a]α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr.hInjective fun a => ↑a
α: Type u_1β: Type ?u.2948γ: Type ?u.2951ι: Sort ?u.2954inst✝: InfSet αs: Set αx: αhx: x ∈ sh: ¬(fun a => ↑a) '' s ⊆ {⊤}intro.inr↑(sInf s) = ↑(sInf ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)))exact Option.some_injective: ∀ (α : Type ?u.4083), Injective Option.someOption.some_injective _: Type ?u.4083_Goals accomplished! 🐙
#align with_top.coe_Inf' WithTop.coe_sInf': ∀ {α : Type u_1} [inst : InfSet α] {s : Set α}, Set.Nonempty s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)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: Sort ?u.4124 → PropNonempty ι: Sort ?u.4121ι] [InfSet: Type ?u.4127 → Type ?u.4127InfSet α: Type ?u.4112α] (f: ι → αf : ι: Sort ?u.4121ι → α: Type ?u.4112α) :
↑(⨅ i: ?m.4258i, f: ι → αf i: ?m.4258i) = (⨅ i: ?m.4159i, f: ι → αf i: ?m.4159i : WithTop: Type ?u.4139 → Type ?u.4139WithTop α: Type ?u.4112α) := byGoals accomplished! 🐙
α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(⨅ i, f i) = ⨅ i, ↑(f i)rw [α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(⨅ i, f i) = ⨅ i, ↑(f i)iInf: {α : Type ?u.4380} → [inst : InfSet α] → {ι : Sort ?u.4379} → (ι → α) → αiInf,α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(sInf (range fun i => f i)) = ⨅ i, ↑(f i) α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(⨅ i, f i) = ⨅ i, ↑(f i)iInf: {α : Type ?u.4432} → [inst : InfSet α] → {ι : Sort ?u.4431} → (ι → α) → αiInf,α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(sInf (range fun i => f i)) = sInf (range fun i => ↑(f i)) α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(⨅ i, f i) = ⨅ i, ↑(f i)WithTop.coe_sInf': ∀ {α : Type ?u.4433} [inst : InfSet α] {s : Set α}, Set.Nonempty s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)WithTop.coe_sInf' (range_nonempty: ∀ {α : Type ?u.4438} {ι : Sort ?u.4437} [h : Nonempty ι] (f : ι → α), Set.Nonempty (range f)range_nonempty f: ι → αf),α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → αsInf ((fun a => ↑a) '' range f) = sInf (range fun i => ↑(f i)) α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(⨅ i, f i) = ⨅ i, ↑(f i)← range_comp: ∀ {α : Type ?u.4481} {β : Type ?u.4479} {ι : Sort ?u.4480} (g : α → β) (f : ι → α), range (g ∘ f) = g '' range frange_compα: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → αsInf (range ((fun a => ↑a) ∘ f)) = sInf (range fun i => ↑(f i))]α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → αsInf (range ((fun a => ↑a) ∘ f)) = sInf (range fun i => ↑(f i));α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → αsInf (range ((fun a => ↑a) ∘ f)) = sInf (range fun i => ↑(f i)) α: Type u_2β: Type ?u.4115γ: Type ?u.4118ι: Sort u_1inst✝¹: Nonempty ιinst✝: InfSet αf: ι → α↑(⨅ i, f i) = ⨅ i, ↑(f i)rflGoals accomplished! 🐙
#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)WithTop.coe_iInf

theorem WithTop.coe_sSup': ∀ [inst : Preorder α] [inst_1 : SupSet α] {s : Set α}, BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)WithTop.coe_sSup' [Preorder: Type ?u.4660 → Type ?u.4660Preorder α: Type ?u.4648α] [SupSet: Type ?u.4663 → Type ?u.4663SupSet α: Type ?u.4648α] {s: Set αs : Set: Type ?u.4666 → Type ?u.4666Set α: Type ?u.4648α} (hs: BddAbove shs : BddAbove: {α : Type ?u.4669} → [inst : Preorder α] → Set α → PropBddAbove s: Set αs) :
↑(sSup: {α : Type ?u.4819} → [self : SupSet α] → Set α → αsSup s: Set αs) = (sSup: {α : Type ?u.4700} → [self : SupSet α] → Set α → αsSup ((fun (a: αa : α: Type ?u.4648α) ↦ ↑a: αa) '' s: Set αs) : WithTop: Type ?u.4699 → Type ?u.4699WithTop α: Type ?u.4648α) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) = sSup ((fun a => ↑a) '' s)change _: ?m.4893_ = ite: {α : Sort ?u.4895} → (c : Prop) → [h : Decidable c] → α → α → αite _: Prop_ _: ?m.4896_ _: ?m.4896_α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) =   if ⊤ ∈ (fun a => ↑a) '' s then ⊤
else if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤
α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) = sSup ((fun a => ↑a) '' s)rw [α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) =   if ⊤ ∈ (fun a => ↑a) '' s then ⊤
else if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.5263} {t e : α}, (if c then t else e) = eif_neg,α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) =   if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' s α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) =   if ⊤ ∈ (fun a => ↑a) '' s then ⊤
else if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤preimage_image_eq: ∀ {α : Type ?u.5283} {β : Type ?u.5284} {f : α → β} (s : Set α), Injective f → f ⁻¹' (f '' s) = spreimage_image_eq,α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) = if BddAbove s then ↑(sSup s) else ⊤α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shInjective fun a => ↑aα: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' s α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) =   if ⊤ ∈ (fun a => ↑a) '' s then ⊤
else if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.5311} {t e : α}, (if c then t else e) = tif_pos hs: BddAbove shsα: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) = ↑(sSup s)α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shInjective fun a => ↑aα: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' s]α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shInjective fun a => ↑aα: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' s
α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) = sSup ((fun a => ↑a) '' s)·α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shInjective fun a => ↑a α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shInjective fun a => ↑aα: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' sexact Option.some_injective: ∀ (α : Type ?u.5324), Injective Option.someOption.some_injective _: Type ?u.5324_Goals accomplished! 🐙
α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove s↑(sSup s) = sSup ((fun a => ↑a) '' s)·α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' s α: Type u_1β: Type ?u.4651γ: Type ?u.4654ι: Sort ?u.4657inst✝¹: Preorder αinst✝: SupSet αs: Set αhs: BddAbove shnc¬⊤ ∈ (fun a => ↑a) '' srintro ⟨x, _, ⟨⟩⟩: ⊤ ∈ (fun a => ↑a) '' s⟨x: αx⟨x, _, ⟨⟩⟩: ⊤ ∈ (fun a => ↑a) '' s, _: x ∈ s_⟨x, _, ⟨⟩⟩: ⊤ ∈ (fun a => ↑a) '' s, ⟨⟩: (fun a => ↑a) x = ⊤⟨⟩⟨x, _, ⟨⟩⟩: ⊤ ∈ (fun a => ↑a) '' s⟩Goals accomplished! 🐙
#align with_top.coe_Sup' WithTop.coe_sSup': ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SupSet α] {s : Set α}, BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)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: ∀ [inst : Preorder α] [inst_1 : SupSet α] (f : ι → α), BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)WithTop.coe_iSup [Preorder: Type ?u.5459 → Type ?u.5459Preorder α: Type ?u.5447α] [SupSet: Type ?u.5462 → Type ?u.5462SupSet α: Type ?u.5447α] (f: ι → αf : ι: Sort ?u.5456ι → α: Type ?u.5447α) (h: BddAbove (range f)h : BddAbove: {α : Type ?u.5469} → [inst : Preorder α] → Set α → PropBddAbove (Set.range: {α : Type ?u.5486} → {ι : Sort ?u.5485} → (ι → α) → Set αSet.range f: ι → αf)) :
↑(⨆ i: ?m.5629i, f: ι → αf i: ?m.5629i) = (⨆ i: ?m.5527i, f: ι → αf i: ?m.5527i : WithTop: Type ?u.5507 → Type ?u.5507WithTop α: Type ?u.5447α) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(⨆ i, f i) = ⨆ i, ↑(f i)rw [α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(⨆ i, f i) = ⨆ i, ↑(f i)iSup: {α : Type ?u.5761} → [inst : SupSet α] → {ι : Sort ?u.5760} → (ι → α) → αiSup,α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(sSup (range fun i => f i)) = ⨆ i, ↑(f i) α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(⨆ i, f i) = ⨆ i, ↑(f i)iSup: {α : Type ?u.5817} → [inst : SupSet α] → {ι : Sort ?u.5816} → (ι → α) → αiSup,α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(sSup (range fun i => f i)) = sSup (range fun i => ↑(f i)) α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(⨆ i, f i) = ⨆ i, ↑(f i)WithTop.coe_sSup': ∀ {α : Type ?u.5818} [inst : Preorder α] [inst_1 : SupSet α] {s : Set α},
BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)WithTop.coe_sSup' h: BddAbove (range f)h,α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)sSup ((fun a => ↑a) '' range f) = sSup (range fun i => ↑(f i)) α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(⨆ i, f i) = ⨆ i, ↑(f i)← range_comp: ∀ {α : Type ?u.5851} {β : Type ?u.5849} {ι : Sort ?u.5850} (g : α → β) (f : ι → α), range (g ∘ f) = g '' range frange_compα: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)sSup (range ((fun a => ↑a) ∘ f)) = sSup (range fun i => ↑(f i))]α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)sSup (range ((fun a => ↑a) ∘ f)) = sSup (range fun i => ↑(f i));α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)sSup (range ((fun a => ↑a) ∘ f)) = sSup (range fun i => ↑(f i)) α: Type u_1β: Type ?u.5450γ: Type ?u.5453ι: Sort u_2inst✝¹: Preorder αinst✝: SupSet αf: ι → αh: BddAbove (range f)↑(⨆ i, f i) = ⨆ i, ↑(f i)rflGoals accomplished! 🐙
#align with_top.coe_supr WithTop.coe_iSup: ∀ {α : Type u_1} {ι : Sort u_2} [inst : Preorder α] [inst_1 : SupSet α] (f : ι → α),
BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)WithTop.coe_iSup

@[simp]
theorem WithBot.csSup_empty: ∀ {α : Type u_1} [inst : SupSet α], sSup ∅ = ⊥WithBot.csSup_empty {α: Type u_1α : Type _: Type (?u.6040+1)Type _} [SupSet: Type ?u.6043 → Type ?u.6043SupSet α: Type ?u.6040α] : sSup: {α : Type ?u.6047} → [self : SupSet α] → Set α → αsSup (∅: ?m.6054∅ : Set: Type ?u.6051 → Type ?u.6051Set (WithBot: Type ?u.6052 → Type ?u.6052WithBot α: Type ?u.6040α)) = ⊥: ?m.6112⊥ :=
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.6164} {t e : α}, (if c then t else e) = tif_pos <| Set.empty_subset: ∀ {α : Type ?u.6167} (s : Set α), ∅ ⊆ sSet.empty_subset _: Set ?m.6168_
#align with_bot.cSup_empty WithBot.csSup_empty: ∀ {α : Type u_1} [inst : SupSet α], sSup ∅ = ⊥WithBot.csSup_empty

@[simp]
theorem WithBot.ciSup_empty: ∀ {α : Type u_1} [inst : IsEmpty ι] [inst : SupSet α] (f : ι → WithBot α), (⨆ i, f i) = ⊥WithBot.ciSup_empty {α: Type ?u.6226α : Type _: Type (?u.6226+1)Type _} [IsEmpty: Sort ?u.6229 → PropIsEmpty ι: Sort ?u.6223ι] [SupSet: Type ?u.6232 → Type ?u.6232SupSet α: Type ?u.6226α] (f: ι → WithBot αf : ι: Sort ?u.6223ι → WithBot: Type ?u.6237 → Type ?u.6237WithBot α: Type ?u.6226α) :
(⨆ i: ?m.6248i, f: ι → WithBot αf i: ?m.6248i) = ⊥: ?m.6268⊥ :=
@WithTop.iInf_empty: ∀ {ι : Sort ?u.6324} {α : Type ?u.6323} [inst : IsEmpty ι] [inst : InfSet α] (f : ι → WithTop α), (⨅ i, f i) = ⊤WithTop.iInf_empty _: Sort ?u.6324_ α: Type u_1αᵒᵈ _ _ _: ?m.6325 → WithTop αᵒᵈ_
#align with_bot.csupr_empty WithBot.ciSup_empty: ∀ {ι : Sort u_2} {α : Type u_1} [inst : IsEmpty ι] [inst : SupSet α] (f : ι → WithBot α), (⨆ i, f i) = ⊥WithBot.ciSup_empty

@[norm_cast]
theorem WithBot.coe_sSup': ∀ {α : Type u_1} [inst : SupSet α] {s : Set α}, Set.Nonempty s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)WithBot.coe_sSup' [SupSet: Type ?u.6446 → Type ?u.6446SupSet α: Type ?u.6434α] {s: Set αs : Set: Type ?u.6449 → Type ?u.6449Set α: Type ?u.6434α} (hs: Set.Nonempty shs : s: Set αs.Nonempty: {α : Type ?u.6452} → Set α → PropNonempty) :
↑(sSup: {α : Type ?u.6589} → [self : SupSet α] → Set α → αsSup s: Set αs) = (sSup: {α : Type ?u.6465} → [self : SupSet α] → Set α → αsSup ((fun (a: αa : α: Type ?u.6434α) ↦ ↑a: αa) '' s: Set αs) : WithBot: Type ?u.6464 → Type ?u.6464WithBot α: Type ?u.6434α) :=
@WithTop.coe_sInf': ∀ {α : Type ?u.6661} [inst : InfSet α] {s : Set α}, Set.Nonempty s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)WithTop.coe_sInf' α: Type ?u.6434αᵒᵈ _ _: Set αᵒᵈ_ hs: Set.Nonempty shs
#align with_bot.coe_Sup' WithBot.coe_sSup': ∀ {α : Type u_1} [inst : SupSet α] {s : Set α}, Set.Nonempty s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)WithBot.coe_sSup'

@[norm_cast]
theorem WithBot.coe_iSup: ∀ [inst : Nonempty ι] [inst : SupSet α] (f : ι → α), ↑(⨆ i, f i) = ⨆ i, ↑(f i)WithBot.coe_iSup [Nonempty: Sort ?u.6875 → PropNonempty ι: Sort ?u.6872ι] [SupSet: Type ?u.6878 → Type ?u.6878SupSet α: Type ?u.6863α] (f: ι → αf : ι: Sort ?u.6872ι → α: Type ?u.6863α) :
↑(⨆ i: ?m.7017i, f: ι → αf i: ?m.7017i) = (⨆ i: ?m.6910i, f: ι → αf i: ?m.6910i : WithBot: Type ?u.6890 → Type ?u.6890WithBot α: Type ?u.6863α) :=
@WithTop.coe_iInf: ∀ {α : Type ?u.7090} {ι : Sort ?u.7089} [inst : Nonempty ι] [inst : InfSet α] (f : ι → α), ↑(⨅ i, f i) = ⨅ i, ↑(f i)WithTop.coe_iInf α: Type ?u.6863αᵒᵈ _: Sort ?u.7089_ _ _ _: ?m.7092 → αᵒᵈ_
#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)WithBot.coe_iSup

@[norm_cast]
theorem WithBot.coe_sInf': ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : InfSet α] {s : Set α}, BddBelow s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)WithBot.coe_sInf' [Preorder: Type ?u.7309 → Type ?u.7309Preorder α: Type ?u.7297α] [InfSet: Type ?u.7312 → Type ?u.7312InfSet α: Type ?u.7297α] {s: Set αs : Set: Type ?u.7315 → Type ?u.7315Set α: Type ?u.7297α} (hs: BddBelow shs : BddBelow: {α : Type ?u.7318} → [inst : Preorder α] → Set α → PropBddBelow s: Set αs) :
↑(sInf: {α : Type ?u.7476} → [self : InfSet α] → Set α → αsInf s: Set αs) = (sInf: {α : Type ?u.7349} → [self : InfSet α] → Set α → αsInf ((fun (a: αa : α: Type ?u.7297α) ↦ ↑a: αa) '' s: Set αs) : WithBot: Type ?u.7348 → Type ?u.7348WithBot α: Type ?u.7297α) :=
@WithTop.coe_sSup': ∀ {α : Type ?u.7549} [inst : Preorder α] [inst_1 : SupSet α] {s : Set α},
BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)WithTop.coe_sSup' α: Type ?u.7297αᵒᵈ _ _ _: Set αᵒᵈ_ hs: BddBelow shs
#align with_bot.coe_Inf' WithBot.coe_sInf': ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : InfSet α] {s : Set α}, BddBelow s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)WithBot.coe_sInf'

@[norm_cast]
theorem WithBot.coe_iInf: ∀ {α : Type u_1} {ι : Sort u_2} [inst : Preorder α] [inst_1 : InfSet α] (f : ι → α),
BddBelow (range f) → ↑(⨅ i, f i) = ⨅ i, ↑(f i)WithBot.coe_iInf [Preorder: Type ?u.7799 → Type ?u.7799Preorder α: Type ?u.7787α] [InfSet: Type ?u.7802 → Type ?u.7802InfSet α: Type ?u.7787α] (f: ι → αf : ι: Sort ?u.7796ι → α: Type ?u.7787α) (h: BddBelow (range f)h : BddBelow: {α : Type ?u.7809} → [inst : Preorder α] → Set α → PropBddBelow (Set.range: {α : Type ?u.7826} → {ι : Sort ?u.7825} → (ι → α) → Set αSet.range f: ι → αf)) :
↑(⨅ i: ?m.7977i, f: ι → αf i: ?m.7977i) = (⨅ i: ?m.7867i, f: ι → αf i: ?m.7867i : WithBot: Type ?u.7847 → Type ?u.7847WithBot α: Type ?u.7787α) :=
@WithTop.coe_iSup: ∀ {α : Type ?u.8050} {ι : Sort ?u.8051} [inst : Preorder α] [inst_1 : SupSet α] (f : ι → α),
BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)WithTop.coe_iSup α: Type ?u.7787αᵒᵈ _: Sort ?u.8051_ _ _ _: ?m.8053 → αᵒᵈ_ h: BddBelow (range f)h
#align with_bot.coe_infi WithBot.coe_iInf: ∀ {α : Type u_1} {ι : Sort u_2} [inst : Preorder α] [inst_1 : InfSet α] (f : ι → α),
BddBelow (range f) → ↑(⨅ i, f i) = ⨅ i, ↑(f i)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 u_1} →
[toLattice : Lattice α] →
[toSupSet : SupSet α] →
[toInfSet : InfSet α] →
(∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ SupSet.sSup s) →
(∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ upperBounds s → SupSet.sSup s ≤ a) →
(∀ (s : Set α) (a : α), BddBelow s → a ∈ s → InfSet.sInf s ≤ a) →
(∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ lowerBounds s → a ≤ InfSet.sInf s) →
ConditionallyCompleteLattice αConditionallyCompleteLattice (α: Type ?u.8259α : Type _: Type (?u.8259+1)Type _) extends Lattice: Type ?u.8264 → Type ?u.8264Lattice α: Type ?u.8259α, SupSet: Type ?u.8312 → Type ?u.8312SupSet α: Type ?u.8259α, InfSet: Type ?u.8316 → Type ?u.8316InfSet α: Type ?u.8259α where
/-- `a ≤ sSup s` for all `a ∈ s`. -/
le_csSup: ∀ {α : Type u_1} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ SupSet.sSup sle_csSup : ∀ s: ?m.8321s a: ?m.8324a, BddAbove: {α : Type ?u.8328} → [inst : Preorder α] → Set α → PropBddAbove s: ?m.8321s → a: ?m.8324a ∈ s: ?m.8321s → a: ?m.8324a ≤ sSup: Set α → αsSup s: ?m.8321s
/-- `sSup s ≤ a` for all `a ∈ upperBounds s`. -/
csSup_le: ∀ {α : Type u_1} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α),
Set.Nonempty s → a ∈ upperBounds s → SupSet.sSup s ≤ acsSup_le : ∀ s: ?m.8425s a: ?m.8428a, Set.Nonempty: {α : Type ?u.8432} → Set α → PropSet.Nonempty s: ?m.8425s → a: ?m.8428a ∈ upperBounds: {α : Type ?u.8453} → [inst : Preorder α] → Set α → Set αupperBounds s: ?m.8425s → sSup: Set α → αsSup s: ?m.8425s ≤ a: ?m.8428a
/-- `sInf s ≤ a` for all `a ∈ s`. -/
csInf_le: ∀ {α : Type u_1} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α), BddBelow s → a ∈ s → InfSet.sInf s ≤ acsInf_le : ∀ s: ?m.8526s a: ?m.8529a, BddBelow: {α : Type ?u.8533} → [inst : Preorder α] → Set α → PropBddBelow s: ?m.8526s → a: ?m.8529a ∈ s: ?m.8526s → sInf: Set α → αsInf s: ?m.8526s ≤ a: ?m.8529a
/-- `a ≤ sInf s` for all `a ∈ lowerBounds s`. -/
le_csInf: ∀ {α : Type u_1} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α),
Set.Nonempty s → a ∈ lowerBounds s → a ≤ InfSet.sInf sle_csInf : ∀ s: ?m.8621s a: ?m.8624a, Set.Nonempty: {α : Type ?u.8628} → Set α → PropSet.Nonempty s: ?m.8621s → a: ?m.8624a ∈ lowerBounds: {α : Type ?u.8649} → [inst : Preorder α] → Set α → Set αlowerBounds s: ?m.8621s → a: ?m.8624a ≤ sInf: Set α → αsInf s: ?m.8621s
#align conditionally_complete_lattice ConditionallyCompleteLattice: Type u_1 → Type u_1ConditionallyCompleteLattice

-- 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 u_1} →
[toConditionallyCompleteLattice : ConditionallyCompleteLattice α] →
(∀ (a b : α), a ≤ b ∨ b ≤ a) →
(DecidableRel fun x x_1 => x ≤ x_1) →
DecidableEq α → (DecidableRel fun x x_1 => x < x_1) → ConditionallyCompleteLinearOrder αConditionallyCompleteLinearOrder (α: Type ?u.8828α : Type _: Type (?u.8828+1)Type _) extends ConditionallyCompleteLattice: Type ?u.8833 → Type ?u.8833ConditionallyCompleteLattice α: Type ?u.8828α where
/-- A `ConditionallyCompleteLinearOrder` is total. -/
le_total: ∀ {α : Type u_1} [self : ConditionallyCompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ ale_total (a: αa b: αb : α: Type ?u.8828α) : a: αa ≤ b: αb ∨ b: αb ≤ a: αa
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
decidableLE: {α : Type u_1} → [self : ConditionallyCompleteLinearOrder α] → DecidableRel fun x x_1 => x ≤ x_1decidableLE : DecidableRel: {α : Sort ?u.8922} → (α → α → Prop) → Sort (max1?u.8922)DecidableRel (. ≤ . : α: Type ?u.8828α → α: Type ?u.8828α → Prop: TypeProp)
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
decidableEq: {α : Type u_1} → [self : ConditionallyCompleteLinearOrder α] → DecidableEq αdecidableEq : DecidableEq: Sort ?u.8948 → Sort (max1?u.8948)DecidableEq α: Type ?u.8828α := @decidableEqOfDecidableLE: {α : Type ?u.8949} → [inst : PartialOrder α] → [inst : DecidableRel fun x x_1 => x ≤ x_1] → DecidableEq αdecidableEqOfDecidableLE _: Type ?u.8949_ _ decidableLE: DecidableRel fun x x_1 => x ≤ x_1decidableLE
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
decidableLT: {α : Type u_1} → [self : ConditionallyCompleteLinearOrder α] → DecidableRel fun x x_1 => x < x_1decidableLT : DecidableRel: {α : Sort ?u.9001} → (α → α → Prop) → Sort (max1?u.9001)DecidableRel (. < . : α: Type ?u.8828α → α: Type ?u.8828α → Prop: TypeProp) :=
@decidableLTOfDecidableLE: {α : Type ?u.9027} →
[inst : Preorder α] → [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] → DecidableRel fun x x_1 => x < x_1decidableLTOfDecidableLE _: Type ?u.9027_ _ decidableLE: DecidableRel fun x x_1 => x ≤ x_1decidableLE
#align conditionally_complete_linear_order ConditionallyCompleteLinearOrder: Type u_1 → Type u_1ConditionallyCompleteLinearOrder

instance: (α : Type u_1) → [inst : ConditionallyCompleteLinearOrder α] → LinearOrder αinstance (α: Type ?u.9857α : Type _: Type (?u.9857+1)Type _) [ConditionallyCompleteLinearOrder: Type ?u.9860 → Type ?u.9860ConditionallyCompleteLinearOrder α: Type ?u.9857α] : LinearOrder: Type ?u.9863 → Type ?u.9863LinearOrder α: Type ?u.9857α :=
{ ‹ConditionallyCompleteLinearOrder α› with
max := Sup.sup: {α : Type ?u.9938} → [self : Sup α] → α → α → αSup.sup, min := Inf.inf: {α : Type ?u.9892} → [self : Inf α] → α → α → αInf.inf,
min_def := fun a: ?m.10016a b: ?m.10019b ↦ byGoals accomplished! 🐙
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αmin a b = if a ≤ b then a else bby_cases hab: ?m.10097hab : a: αa = b: αbα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: a = bposmin a b = if a ≤ b then a else bα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmin a b = if a ≤ b then a else b
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αmin a b = if a ≤ b then a else b·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: a = bposmin a b = if a ≤ b then a else b α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: a = bposmin a b = if a ≤ b then a else bα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmin a b = if a ≤ b then a else bsimp [hab: ?m.10090hab]Goals accomplished! 🐙
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αmin a b = if a ≤ b then a else b·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmin a b = if a ≤ b then a else b α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmin a b = if a ≤ b then a else brcases ConditionallyCompleteLinearOrder.le_total: ∀ {α : Type ?u.10361} [self : ConditionallyCompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ aConditionallyCompleteLinearOrder.le_total a: αa b: αb with (h₁ | h₂): a ≤ b ∨ b ≤ a(h₁: a ≤ bh₁h₁ | h₂: a ≤ b ∨ b ≤ a | h₂: b ≤ ah₂(h₁ | h₂): a ≤ b ∨ b ≤ a)α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₁: a ≤ bneg.inlmin a b = if a ≤ b then a else bα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmin a b = if a ≤ b then a else b
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmin a b = if a ≤ b then a else b·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₁: a ≤ bneg.inlmin a b = if a ≤ b then a else b α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₁: a ≤ bneg.inlmin a b = if a ≤ b then a else bα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmin a b = if a ≤ b then a else bsimp [h₁: a ≤ bh₁]Goals accomplished! 🐙
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmin a b = if a ≤ b then a else b·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmin a b = if a ≤ b then a else b α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmin a b = if a ≤ b then a else bsimp [show ¬(a: αa ≤ b: αb) from fun h: ?m.10699h => hab: ?m.10097hab (le_antisymm: ∀ {α : Type ?u.10701} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm h: ?m.10699h h₂: b ≤ ah₂), h₂: b ≤ ah₂]Goals accomplished! 🐙
max_def := fun a: ?m.10031a b: ?m.10034b ↦ byGoals accomplished! 🐙
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αmax a b = if a ≤ b then b else aby_cases hab: ?m.11180hab : a: αa = b: αbα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: a = bposmax a b = if a ≤ b then b else aα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmax a b = if a ≤ b then b else a
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αmax a b = if a ≤ b then b else a·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: a = bposmax a b = if a ≤ b then b else a α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: a = bposmax a b = if a ≤ b then b else aα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmax a b = if a ≤ b then b else asimp [hab: ?m.11173hab]Goals accomplished! 🐙
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αmax a b = if a ≤ b then b else a·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmax a b = if a ≤ b then b else a α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmax a b = if a ≤ b then b else arcases ConditionallyCompleteLinearOrder.le_total: ∀ {α : Type ?u.11441} [self : ConditionallyCompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ aConditionallyCompleteLinearOrder.le_total a: αa b: αb with (h₁ | h₂): a ≤ b ∨ b ≤ a(h₁: a ≤ bh₁h₁ | h₂: a ≤ b ∨ b ≤ a | h₂: b ≤ ah₂(h₁ | h₂): a ≤ b ∨ b ≤ a)α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₁: a ≤ bneg.inlmax a b = if a ≤ b then b else aα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmax a b = if a ≤ b then b else a
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmax a b = if a ≤ b then b else a·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₁: a ≤ bneg.inlmax a b = if a ≤ b then b else a α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₁: a ≤ bneg.inlmax a b = if a ≤ b then b else aα✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmax a b = if a ≤ b then b else asimp [h₁: a ≤ bh₁]Goals accomplished! 🐙
α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bnegmax a b = if a ≤ b then b else a·α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmax a b = if a ≤ b then b else a α✝: Type ?u.9845β: Type ?u.9848γ: Type ?u.9851ι: Sort ?u.9854α: Type ?u.10043inst✝: ConditionallyCompleteLinearOrder αsrc✝:= inst✝: ConditionallyCompleteLinearOrder αa, b: αhab: ¬a = bh₂: b ≤ aneg.inrmax a b = if a ≤ b then b else asimp [show ¬(a: αa ≤ b: αb) from fun h: ?m.11895h => hab: ?m.11180hab (le_antisymm: ∀ {α : Type ?u.11897} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm h: ?m.11895h h₂: b ≤ ah₂), h₂: b ≤ ah₂]Goals accomplished! 🐙 }

/-- 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 u_1} →
[toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α] →
[toBot : Bot α] → (∀ (x : α), ⊥ ≤ x) → SupSet.sSup ∅ = ⊥ → ConditionallyCompleteLinearOrderBot αConditionallyCompleteLinearOrderBot (α: Type ?u.12582α : Type _: Type (?u.12582+1)Type _) extends ConditionallyCompleteLinearOrder: Type ?u.12587 → Type ?u.12587ConditionallyCompleteLinearOrder α: Type ?u.12582α,
Bot: Type ?u.12671 → Type ?u.12671Bot α: Type ?u.12582α where
/-- `⊥` is the least element -/
bot_le: ∀ {α : Type u_1} [self : ConditionallyCompleteLinearOrderBot α] (x : α), ⊥ ≤ xbot_le : ∀ x: αx : α: Type ?u.12582α, ⊥: ?m.12680⊥ ≤ x: αx
/-- The supremum of the empty set is `⊥` -/
csSup_empty: ∀ {α : Type u_1} [self : ConditionallyCompleteLinearOrderBot α], SupSet.sSup ∅ = ⊥csSup_empty : sSup: Set α → αsSup ∅: ?m.12742∅ = ⊥: ?m.12785⊥
#align conditionally_complete_linear_order_bot ConditionallyCompleteLinearOrderBot: Type u_1 → Type u_1ConditionallyCompleteLinearOrderBot

-- see Note [lower instance priority]
instance (priority := 100) ConditionallyCompleteLinearOrderBot.toOrderBot: [h : ConditionallyCompleteLinearOrderBot α] → OrderBot αConditionallyCompleteLinearOrderBot.toOrderBot
[h: ConditionallyCompleteLinearOrderBot αh : ConditionallyCompleteLinearOrderBot: Type ?u.12918 → Type ?u.12918ConditionallyCompleteLinearOrderBot α: Type ?u.12906α] : OrderBot: (α : Type ?u.12921) → [inst : LE α] → Type ?u.12921OrderBot α: Type ?u.12906α :=
{ h: ConditionallyCompleteLinearOrderBot αh with }
#align conditionally_complete_linear_order_bot.to_order_bot ConditionallyCompleteLinearOrderBot.toOrderBot: {α : Type u_1} → [h : ConditionallyCompleteLinearOrderBot α] → OrderBot α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: {α : Type u_1} → [inst : CompleteLattice α] → ConditionallyCompleteLattice αCompleteLattice.toConditionallyCompleteLattice [CompleteLattice: Type ?u.13165 → Type ?u.13165CompleteLattice α: Type ?u.13153α] :
ConditionallyCompleteLattice: Type ?u.13168 → Type ?u.13168ConditionallyCompleteLattice α: Type ?u.13153α :=
{ ‹CompleteLattice α› with
le_csSup := byGoals accomplished! 🐙 α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup sintrosα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddAbove s✝a✝: a✝² ∈ s✝a✝² ≤ sSup s✝;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddAbove s✝a✝: a✝² ∈ s✝a✝² ≤ sSup s✝ α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup sapply le_sSup: ∀ {α : Type ?u.13214} [self : CompleteLattice α] (s : Set α) (a : α), a ∈ s → a ≤ sSup sle_sSupα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddAbove s✝a✝: a✝² ∈ s✝aa✝² ∈ s✝;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddAbove s✝a✝: a✝² ∈ s✝aa✝² ∈ s✝ α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup sassumptionGoals accomplished! 🐙
csSup_le := byGoals accomplished! 🐙 α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ aintrosα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ upperBounds s✝sSup s✝ ≤ a✝²;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ upperBounds s✝sSup s✝ ≤ a✝² α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ aapply sSup_le: ∀ {α : Type ?u.13254} [self : CompleteLattice α] (s : Set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → sSup s ≤ asSup_leα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ upperBounds s✝a∀ (b : α), b ∈ s✝ → b ≤ a✝²;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ upperBounds s✝a∀ (b : α), b ∈ s✝ → b ≤ a✝² α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ aassumptionGoals accomplished! 🐙
csInf_le := byGoals accomplished! 🐙 α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ aintrosα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddBelow s✝a✝: a✝² ∈ s✝sInf s✝ ≤ a✝²;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddBelow s✝a✝: a✝² ∈ s✝sInf s✝ ≤ a✝² α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ aapply sInf_le: ∀ {α : Type ?u.13287} [self : CompleteLattice α] (s : Set α) (a : α), a ∈ s → sInf s ≤ asInf_leα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddBelow s✝a✝: a✝² ∈ s✝aa✝² ∈ s✝;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: BddBelow s✝a✝: a✝² ∈ s✝aa✝² ∈ s✝ α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ aassumptionGoals accomplished! 🐙
le_csInf := byGoals accomplished! 🐙 α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf sintrosα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ lowerBounds s✝a✝² ≤ sInf s✝;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ lowerBounds s✝a✝² ≤ sInf s✝ α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf sapply le_sInf: ∀ {α : Type ?u.13322} [self : CompleteLattice α] (s : Set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ sInf sle_sInfα: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ lowerBounds s✝a∀ (b : α), b ∈ s✝ → a✝² ≤ b;α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice αs✝: Set αa✝²: αa✝¹: Set.Nonempty s✝a✝: a✝² ∈ lowerBounds s✝a∀ (b : α), b ∈ s✝ → a✝² ≤ b α: Type ?u.13153β: Type ?u.13156γ: Type ?u.13159ι: Sort ?u.13162inst✝: CompleteLattice αsrc✝:= inst✝: CompleteLattice α∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf sassumptionGoals accomplished! 🐙 }
#align complete_lattice.to_conditionally_complete_lattice CompleteLattice.toConditionallyCompleteLattice: {α : Type u_1} → [inst : CompleteLattice α] → ConditionallyCompleteLattice αCompleteLattice.toConditionallyCompleteLattice

-- see Note [lower instance priority]
instance (priority := 100) CompleteLinearOrder.toConditionallyCompleteLinearOrderBot: {α : Type u_1} → [h : CompleteLinearOrder α] → ConditionallyCompleteLinearOrderBot αCompleteLinearOrder.toConditionallyCompleteLinearOrderBot {α: Type ?u.13465α : Type _: Type (?u.13465+1)Type _}
[h: CompleteLinearOrder αh : CompleteLinearOrder: Type ?u.13468 → Type ?u.13468CompleteLinearOrder α: Type ?u.13465α] : ConditionallyCompleteLinearOrderBot: Type ?u.13471 → Type ?u.13471ConditionallyCompleteLinearOrderBot α: Type ?u.13465α :=
{ CompleteLattice.toConditionallyCompleteLattice: {α : Type ?u.13477} → [inst : CompleteLattice α] → ConditionallyCompleteLattice αCompleteLattice.toConditionallyCompleteLattice, h: CompleteLinearOrder αh with csSup_empty := sSup_empty: ∀ {α : Type ?u.13653} [inst : CompleteLattice α], sSup ∅ = ⊥sSup_empty }
#align complete_linear_order.to_conditionally_complete_linear_order_bot CompleteLinearOrder.toConditionallyCompleteLinearOrderBot: {α : Type u_1} → [h : CompleteLinearOrder α] → ConditionallyCompleteLinearOrderBot αCompleteLinearOrder.toConditionallyCompleteLinearOrderBot

section

open Classical

/-- A well founded linear order is conditionally complete, with a bottom element. -/
@[reducible]
noncomputable def IsWellOrder.conditionallyCompleteLinearOrderBot: (α : Type u_1) →
[i₁ : LinearOrder α] →
[i₂ : OrderBot α] → [h : IsWellOrder α fun x x_1 => x < x_1] → ConditionallyCompleteLinearOrderBot αIsWellOrder.conditionallyCompleteLinearOrderBot (α: Type ?u.13816α : Type _: Type (?u.13816+1)Type _)
[i₁: LinearOrder αi₁ : _root_.LinearOrder: Type ?u.13819 → Type ?u.13819_root_.LinearOrder α: Type ?u.13816α] [i₂: OrderBot αi₂ : OrderBot: (α : Type ?u.13822) → [inst : LE α] → Type ?u.13822OrderBot α: Type ?u.13816α] [h: IsWellOrder α fun x x_1 => x < x_1h : IsWellOrder: (α : Type ?u.13996) → (α → α → Prop) → PropIsWellOrder α: Type ?u.13816α (· < ·): α → α → Prop(· < ·)] :
ConditionallyCompleteLinearOrderBot: Type ?u.14135 → Type ?u.14135ConditionallyCompleteLinearOrderBot α: Type ?u.13816α :=
{ i₁: LinearOrder αi₁, i₂: OrderBot αi₂, LinearOrder.toLattice: {α : Type ?u.14143} → [o : LinearOrder α] → Lattice αLinearOrder.toLattice with
sInf := fun s: ?m.14485s => if hs: ?m.14498hs : s: ?m.14485s.Nonempty: {α : Type ?u.14487} → Set α → PropNonempty then h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.14507} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.min: {α : Type ?u.14514} → {r : α → α → Prop} → WellFounded r → (s : Set α) → Set.Nonempty s → αmin s: ?m.14485s hs: ?m.14498hs else ⊥: ?m.14533⊥
csInf_le := fun s: ?m.14607s a: ?m.14610a _: ?m.14613_ has: ?m.14616has => byGoals accomplished! 🐙
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: BddBelow shas: a ∈ ssInf s ≤ ahave s_ne: Set.Nonempty ss_ne : s: Set αs.Nonempty: {α : Type ?u.15970} → Set α → PropNonempty := ⟨a: αa, has: a ∈ shas⟩α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: BddBelow shas: a ∈ ss_ne: Set.Nonempty ssInf s ≤ a
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: BddBelow shas: a ∈ ssInf s ≤ asimpa [s_ne: Set.Nonempty ss_ne] using not_lt: ∀ {α : Type ?u.16349} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ anot_lt.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 (h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.16375} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.not_lt_min: ∀ {α : Type ?u.16382} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : Set.Nonempty s) {x : α},
x ∈ s → ¬r x (WellFounded.min H s h)not_lt_min s: Set αs s_ne: Set.Nonempty ss_ne has: a ∈ shas)Goals accomplished! 🐙
le_csInf := fun s: ?m.14633s a: ?m.14636a hs: ?m.14639hs has: ?m.14642has => byGoals accomplished! 🐙
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: Set.Nonempty shas: a ∈ lowerBounds sa ≤ sInf ssimp only [hs: Set.Nonempty shs, dif_pos: ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort ?u.16559} {t : c → α} {e : ¬c → α}, dite c t e = t hcdif_pos]α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: Set.Nonempty shas: a ∈ lowerBounds sa ≤ WellFounded.min (_ : WellFounded fun x x_1 => x < x_1) s (_ : Set.Nonempty s)
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: Set.Nonempty shas: a ∈ lowerBounds sa ≤ sInf sexact has: a ∈ lowerBounds shas (h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.16700} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.min_mem: ∀ {α : Type ?u.16707} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : Set.Nonempty s), WellFounded.min H s h ∈ smin_mem s: Set αs hs: Set.Nonempty shs)Goals accomplished! 🐙
sSup := fun s: ?m.14219s => if hs: ?m.14336hs : (upperBounds: {α : Type ?u.14221} → [inst : Preorder α] → Set α → Set αupperBounds s: ?m.14219s).Nonempty: {α : Type ?u.14276} → Set α → PropNonempty then h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.14302} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.min: {α : Type ?u.14313} → {r : α → α → Prop} → WellFounded r → (s : Set α) → Set.Nonempty s → αmin _: Set ?m.14319_ hs: ?m.14289hs else ⊥: ?m.14339⊥
le_csSup := fun s: ?m.14559s a: ?m.14562a hs: ?m.14565hs has: ?m.14568has => byGoals accomplished! 🐙
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: BddAbove shas: a ∈ sa ≤ sSup shave h's: Set.Nonempty (upperBounds s)h's : (upperBounds: {α : Type ?u.14853} → [inst : Preorder α] → Set α → Set αupperBounds s: Set αs).Nonempty: {α : Type ?u.14859} → Set α → PropNonempty := hs: BddAbove shsα✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: BddAbove shas: a ∈ sh's: Set.Nonempty (upperBounds s)a ≤ sSup s
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: BddAbove shas: a ∈ sa ≤ sSup ssimp only [h's: Set.Nonempty (upperBounds s)h's, dif_pos: ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort ?u.14900} {t : c → α} {e : ¬c → α}, dite c t e = t hcdif_pos]α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: BddAbove shas: a ∈ sh's: Set.Nonempty (upperBounds s)a ≤ WellFounded.min (_ : WellFounded fun x x_1 => x < x_1) (upperBounds s) (_ : Set.Nonempty (upperBounds s))
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αhs: BddAbove shas: a ∈ sa ≤ sSup sexact h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.15158} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.min_mem: ∀ {α : Type ?u.15165} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : Set.Nonempty s), WellFounded.min H s h ∈ smin_mem _: Set ?m.15171_ h's: Set.Nonempty (upperBounds s)h's has: a ∈ shasGoals accomplished! 🐙
csSup_le := fun s: ?m.14585s a: ?m.14588a _: ?m.14591_ has: ?m.14594has => byGoals accomplished! 🐙
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: Set.Nonempty shas: a ∈ upperBounds ssSup s ≤ ahave h's: Set.Nonempty (upperBounds s)h's : (upperBounds: {α : Type ?u.15184} → [inst : Preorder α] → Set α → Set αupperBounds s: Set αs).Nonempty: {α : Type ?u.15190} → Set α → PropNonempty := ⟨a: αa, has: a ∈ upperBounds shas⟩α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: Set.Nonempty shas: a ∈ upperBounds sh's: Set.Nonempty (upperBounds s)sSup s ≤ a
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: Set.Nonempty shas: a ∈ upperBounds ssSup s ≤ asimp only [h's: Set.Nonempty (upperBounds s)h's, dif_pos: ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort ?u.15215} {t : c → α} {e : ¬c → α}, dite c t e = t hcdif_pos]α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: Set.Nonempty shas: a ∈ upperBounds sh's: Set.Nonempty (upperBounds s)WellFounded.min (_ : WellFounded fun x x_1 => x < x_1) (upperBounds s) (_ : Set.Nonempty (upperBounds s)) ≤ a
α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αs: Set αa: αx✝: Set.Nonempty shas: a ∈ upperBounds ssSup s ≤ asimpa using h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.15651} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.not_lt_min: ∀ {α : Type ?u.15658} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : Set.Nonempty s) {x : α},
x ∈ s → ¬r x (WellFounded.min H s h)not_lt_min _: Set ?m.15667_ h's: Set.Nonempty (upperBounds s)h's has: a ∈ upperBounds shasGoals accomplished! 🐙
csSup_empty := byGoals accomplished! 🐙 α✝: Type ?u.13804β: Type ?u.13807γ: Type ?u.13810ι: Sort ?u.13813α: Type ?u.13816i₁: LinearOrder αi₂: OrderBot αh: IsWellOrder α fun x x_1 => x < x_1src✝:= LinearOrder.toLattice: Lattice αsSup ∅ = ⊥simpa using eq_bot_iff: ∀ {α : Type ?u.21136} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a = ⊥ ↔ a ≤ ⊥eq_bot_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 (not_lt: ∀ {α : Type ?u.21176} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ anot_lt.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 <| h: IsWellOrder α fun x x_1 => x < x_1h.wf: ∀ {α : Type ?u.21264} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded rwf.not_lt_min: ∀ {α : Type ?u.21271} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : Set.Nonempty s) {x : α},
x ∈ s → ¬r x (WellFounded.min H s h)not_lt_min _: Set ?m.21280_ _: Set.Nonempty ?m.21286_ <| mem_univ: ∀ {α : Type ?u.21294} (x : α), x ∈ univmem_univ ⊥: ?m.21297⊥)Goals accomplished! 🐙 }
#align is_well_order.conditionally_complete_linear_order_bot IsWellOrder.conditionallyCompleteLinearOrderBot: (α : Type u_1) →
[i₁ : LinearOrder α] →
[i₂ : OrderBot α] → [h : IsWellOrder α fun x x_1 => x < x_1] → ConditionallyCompleteLinearOrderBot αIsWellOrder.conditionallyCompleteLinearOrderBot

end

section OrderDual

instance: (α : Type u_1) → [inst : ConditionallyCompleteLattice α] → ConditionallyCompleteLattice αᵒᵈinstance (α: Type ?u.21975α : Type _: Type (?u.21975+1)Type _) [ConditionallyCompleteLattice: Type ?u.21978 → Type ?u.21978ConditionallyCompleteLattice α: Type ?u.21975α] : ConditionallyCompleteLattice: Type ?u.21981 → Type ?u.21981ConditionallyCompleteLattice α: Type ?u.21975αᵒᵈ :=
{ instInfOrderDual: (α : Type ?u.21988) → [inst : Sup α] → Inf αᵒᵈinstInfOrderDual α: Type ?u.21975α, instSupOrderDual: (α : Type ?u.22019) → [inst : Inf α] → Sup αᵒᵈinstSupOrderDual α: Type ?u.21975α, OrderDual.lattice: (α : Type ?u.22040) → [inst : Lattice α] → Lattice αᵒᵈOrderDual.lattice α: Type ?u.21975α with
le_csSup := @ConditionallyCompleteLattice.csInf_le: ∀ {α : Type ?u.22132} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ aConditionallyCompleteLattice.csInf_le α: Type ?u.21975α _
csSup_le := @ConditionallyCompleteLattice.le_csInf: ∀ {α : Type ?u.22166} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α),
Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf sConditionallyCompleteLattice.le_csInf α: Type ?u.21975α _
le_csInf := @ConditionallyCompleteLattice.csSup_le: ∀ {α : Type ?u.22198} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α),
Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ aConditionallyCompleteLattice.csSup_le α: Type ?u.21975α _
csInf_le := @ConditionallyCompleteLattice.le_csSup: ∀ {α : Type ?u.22182} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup sConditionallyCompleteLattice.le_csSup α: Type ?u.21975α _ }

instance: (α : Type u_1) → [inst : ConditionallyCompleteLinearOrder α] → ConditionallyCompleteLinearOrder αᵒᵈinstance (α: Type ?u.22302α : Type _: Type (?u.22302+1)Type _) [ConditionallyCompleteLinearOrder: Type ?u.22305 → Type ?u.22305ConditionallyCompleteLinearOrder α: Type ?u.22302α] : ConditionallyCompleteLinearOrder: Type ?u.22308 → Type ?u.22308ConditionallyCompleteLinearOrder α: Type ?u.22302αᵒᵈ :=
{ instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342{ instConditionallyCompleteLatticeOrderDual: (α : Type ?u.22315) → [inst : ConditionallyCompleteLattice α] → ConditionallyCompleteLattice αᵒᵈinstConditionallyCompleteLatticeOrderDual{ instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342 α: Type ?u.22302α{ instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342, OrderDual.linearOrder: (α : Type ?u.22330) → [inst : LinearOrder α] → LinearOrder αᵒᵈOrderDual.linearOrder{ instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342 α: Type ?u.22302α{ instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342 { instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342with{ instConditionallyCompleteLatticeOrderDual α, OrderDual.linearOrder α with }: ConditionallyCompleteLinearOrder ?m.22342 }

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 ?u.22697) →
[H1 : PartialOrder α] →
[H2 : SupSet α] →
(∀ (a b : α), BddAbove {a, b}) →
(∀ (a b : α), BddBelow {a, b}) →
(∀ (s : Set α), BddAbove s → Set.Nonempty s → IsLUB s (sSup s)) → ConditionallyCompleteLattice αconditionallyCompleteLatticeOfsSup (α: Type ?u.22697α : Type _: Type (?u.22697+1)Type _) [H1: PartialOrder αH1 : PartialOrder: Type ?u.22700 → Type ?u.22700PartialOrder α: Type ?u.22697α] [H2: SupSet αH2 : SupSet: Type ?u.22703 → Type ?u.22703SupSet α: Type ?u.22697α]
(bddAbove_pair: ∀ (a b : α), BddAbove {a, b}bddAbove_pair : ∀ a: αa b: αb : α: Type ?u.22697α, BddAbove: {α : Type ?u.22711} → [inst : Preorder α] → Set α → PropBddAbove ({a: αa, b: αb} : Set: Type ?u.22730 → Type ?u.22730Set α: Type ?u.22697α))
(bddBelow_pair: ∀ (a b : α), BddBelow {a, b}bddBelow_pair : ∀ a: αa b: αb : α: Type ?u.22697α, BddBelow: {α : Type ?u.22798} → [inst : Preorder α] → Set α → PropBddBelow ({a: αa, b: αb} : Set: Type ?u.22817 → Type ?u.22817Set α: Type ?u.22697α))
(isLUB_sSup: ∀ (s : Set α), BddAbove s → Set.Nonempty s → IsLUB s (sSup s)isLUB_sSup : ∀ s: Set αs : Set: Type ?u.22849 → Type ?u.22849Set α: Type ?u.22697α, BddAbove: {α : Type ?u.22853} → [inst : Preorder α] → Set α → PropBddAbove s: Set αs → s: Set αs.Nonempty: {α : Type ?u.22875} → Set α → PropNonempty → IsLUB: {α : Type ?u.22880} → [inst : Preorder α] → Set α → α → PropIsLUB s: Set αs (sSup: {α : Type ?u.22900} → [self : SupSet α] → Set α → αsSup s: Set αs)) :
ConditionallyCompleteLattice: Type ?u.22930 → Type ?u.22930ConditionallyCompleteLattice α: Type ?u.22697α :=
{ H1: PartialOrder αH1, H2: SupSet αH2 with
sup := fun a: ?m.22958a b: ?m.22961b => sSup: {α : Type ?u.22963} → [self : SupSet α] → Set α → αsSup {a: ?m.22958a, b: ?m.22961b}
le_sup_left := fun a: ?m.23045a b: ?m.23048b =>
(isLUB_sSup: ∀ (s : Set α), BddAbove s → Set.Nonempty s → IsLUB s (sSup s)isLUB_sSup {a: ?m.23045a, b: ?m.23048b} (bddAbove_pair: ∀ (a b : α), BddAbove {a, b}bddAbove_pair a: ?m.23045a b: ?m.23048b) (insert_nonempty: ∀ {α : Type ?u.23080} (a : α) (s : Set α), Set.Nonempty (insert a s)insert_nonempty _: ?m.23081_ _: Set ?m.23081_)).1: ∀ {a b : Prop}, a ∧ b → a1 (mem_insert: ∀ {α : Type ?u.23101} (x : α) (s : Set α), x ∈ insert x smem_insert _: ?m.23102_ _: Set ?m.23102_)
le_sup_right := fun a: ?m.23120a b: ?m.23123b =>
(isLUB_sSup: ∀ (s : Set α), BddAbove s → Set.Nonempty s → IsLUB s (sSup s)isLUB_sSup {a: ?m.23120a, b: ?m.23123b} (bddAbove_pair: ∀ (a b : α), BddAbove {a, b}bddAbove_pair a: ?m.23120a b: ?m.23123b) (insert_nonempty: ∀ {α : Type ?u.23151} (a : α) (s : Set α), Set.Nonempty (insert a s)insert_nonempty _: ?m.23152_ _: Set ?m.23152_)).1: ∀ {a b : Prop}, a ∧ b → a1
(mem_insert_of_mem: ∀ {α : Type ?u.23158} {x : α} {s : Set α} (y : α), x ∈ s → x ∈ insert y smem_insert_of_mem _: ?m.23159_ (mem_singleton: ∀ {α : Type ?u.23163} (a : α), a ∈ {a}mem_singleton _: ?m.23164_))
sup_le := fun a: ?m.23171a b: ?m.23174b _: ?m.23177_ hac: ?m.23180hac hbc: ?m.23183hbc =>
(isLUB_sSup: ∀ (s : Set α), BddAbove s → Set.Nonempty s → IsLUB s (sSup s)isLUB_sSup {a: ?m.23171a, b: ?m.23174b} (bddAbove_pair: ∀ (a b : α), BddAbove {a, b}bddAbove_pair a: ?m.23171a b: ?m.23174b) (insert_nonempty: ∀ {α : Type ?u.23211} (a : α) (s : Set α), Set.Nonempty (```