Mathlib.Order.CompleteLatticeIntervals

subsetSupSet definition

[Inhabited s] : SupSet s

Full source

/-- `SupSet` structure on a nonempty subset `s` of a preorder with `SupSet`. This definition is
non-canonical (it uses `default s`); it should be used only as here, as an auxiliary instance in the
construction of the `ConditionallyCompleteLinearOrder` structure. -/
noncomputable def subsetSupSet [Inhabited s] : SupSet s where
  sSup t :=
    if ht : t.Nonempty ∧ BddAbove t ∧ sSup ((↑) '' t : Set α) ∈ s
    then ⟨sSup ((↑) '' t : Set α), ht.2.2⟩
    else default

Supremum structure on a subset of a preorder with supremum operator

Informal description

Given a nonempty subset $s$ of a preorder with a supremum operator, this defines a supremum structure on $s$ where the supremum of a subset $t \subseteq s$ is computed as follows: if $t$ is nonempty, bounded above in $s$, and the supremum of the image of $t$ in the ambient preorder lies within $s$, then the supremum is this element; otherwise, it defaults to a specified element of $s$. This definition is auxiliary and should only be used in constructing a conditionally complete linear order structure on $s$.

subset_sSup_def theorem

 [Inhabited s] :
  @sSup s _ = fun t =>
    if ht : t.Nonempty ∧ BddAbove t ∧ sSup ((↑) '' t : Set α) ∈ s then ⟨sSup ((↑) '' t : Set α), ht.2.2⟩ else default

Full source

@[simp]
theorem subset_sSup_def [Inhabited s] :
    @sSup s _ = fun t =>
      if ht : t.Nonempty ∧ BddAbove t ∧ sSup ((↑) '' t : Set α) ∈ s
      then ⟨sSup ((↑) '' t : Set α), ht.2.2⟩
      else default :=
  rfl

Definition of Supremum for Subsets in a Preorder

Informal description

For a nonempty subset $s$ of a preorder with a supremum operator, the supremum of a subset $t \subseteq s$ is defined as follows: if $t$ is nonempty, bounded above in $s$, and the supremum of the image of $t$ in the ambient preorder lies within $s$, then the supremum is this element; otherwise, it defaults to a specified element of $s$.

subset_sSup_of_within theorem

 [Inhabited s] {t : Set s} (h' : t.Nonempty) (h'' : BddAbove t) (h : sSup ((↑) '' t : Set α) ∈ s) :
  sSup ((↑) '' t : Set α) = (@sSup s _ t : α)

Full source

theorem subset_sSup_of_within [Inhabited s] {t : Set s}
    (h' : t.Nonempty) (h'' : BddAbove t) (h : sSupsSup ((↑) '' t : Set α) ∈ s) :
    sSup ((↑) '' t : Set α) = (@sSup s _ t : α) := by simp [dif_pos, h, h', h'']

Supremum in Subtype Equals Supremum in Ambient Order When Contained

Informal description

Let $s$ be a nonempty subset of a conditionally complete linear order $\alpha$, and let $t$ be a nonempty subset of $s$ that is bounded above in $s$. If the supremum of the image of $t$ under the inclusion map $s \hookrightarrow \alpha$ lies within $s$, then this supremum equals the supremum of $t$ in $s$ (viewed as an element of $\alpha$). In other words, for $t \subseteq s$ nonempty and bounded above in $s$, if $\sup(\iota(t)) \in s$ (where $\iota: s \to \alpha$ is the inclusion), then $\sup(\iota(t)) = \iota(\sup_s t)$.

subset_sSup_emptyset theorem

[Inhabited s] : sSup (∅ : Set s) = default

Full source

theorem subset_sSup_emptyset [Inhabited s] :
    sSup (∅ : Set s) = default := by
  simp [sSup]

Supremum of Empty Set in Nonempty Subset Equals Default Element

Informal description

For any nonempty subset $s$ of a preorder with a supremum operator, the supremum of the empty set in $s$ is equal to the default element of $s$.

subset_sSup_of_not_bddAbove theorem

[Inhabited s] {t : Set s} (ht : ¬BddAbove t) : sSup t = default

Full source

theorem subset_sSup_of_not_bddAbove [Inhabited s] {t : Set s} (ht : ¬BddAbove t) :
    sSup t = default := by
  simp [sSup, ht]

Supremum of Unbounded Above Subset Equals Default Element

Informal description

Let $s$ be a nonempty subset of a conditionally complete linear order, and let $t$ be a subset of $s$ that is not bounded above in $s$. Then the supremum of $t$ in $s$ is equal to the default element of $s$.

subsetInfSet definition

[Inhabited s] : InfSet s

Full source

/-- `InfSet` structure on a nonempty subset `s` of a preorder with `InfSet`. This definition is
non-canonical (it uses `default s`); it should be used only as here, as an auxiliary instance in the
construction of the `ConditionallyCompleteLinearOrder` structure. -/
noncomputable def subsetInfSet [Inhabited s] : InfSet s where
  sInf t :=
    if ht : t.Nonempty ∧ BddBelow t ∧ sInf ((↑) '' t : Set α) ∈ s
    then ⟨sInf ((↑) '' t : Set α), ht.2.2⟩
    else default

Infimum structure on a subset of a preorder with infima

Informal description

Given a nonempty subset $s$ of a preorder with an infimum structure, the `subsetInfSet` defines an infimum structure on $s$ where the infimum of a subset $t \subseteq s$ is computed as follows: if $t$ is nonempty, bounded below, and the infimum of the image of $t$ in the ambient type $\alpha$ lies within $s$, then this infimum is used; otherwise, a default element of $s$ is returned. This construction is auxiliary and should only be used in building a `ConditionallyCompleteLinearOrder` structure on $s$.

subset_sInf_def theorem

 [Inhabited s] :
  @sInf s _ = fun t =>
    if ht : t.Nonempty ∧ BddBelow t ∧ sInf ((↑) '' t : Set α) ∈ s then ⟨sInf ((↑) '' t : Set α), ht.2.2⟩ else default

Full source

@[simp]
theorem subset_sInf_def [Inhabited s] :
    @sInf s _ = fun t =>
      if ht : t.Nonempty ∧ BddBelow t ∧ sInf ((↑) '' t : Set α) ∈ s
      then ⟨sInf ((↑) '' t : Set α), ht.2.2⟩ else
      default :=
  rfl

Definition of Infimum Operator on Subset with Default Fallback

Informal description

For a nonempty subset $s$ of a type $\alpha$ with an infimum structure, the infimum operator $\inf$ on $s$ is defined as follows: given a subset $t \subseteq s$, if $t$ is nonempty, bounded below, and the infimum of the image of $t$ in $\alpha$ lies within $s$, then $\inf t$ is this infimum; otherwise, $\inf t$ is the default element of $s$.

subset_sInf_of_within theorem

 [Inhabited s] {t : Set s} (h' : t.Nonempty) (h'' : BddBelow t) (h : sInf ((↑) '' t : Set α) ∈ s) :
  sInf ((↑) '' t : Set α) = (@sInf s _ t : α)

Full source

theorem subset_sInf_of_within [Inhabited s] {t : Set s}
    (h' : t.Nonempty) (h'' : BddBelow t) (h : sInfsInf ((↑) '' t : Set α) ∈ s) :
    sInf ((↑) '' t : Set α) = (@sInf s _ t : α) := by simp [dif_pos, h, h', h'']

Infimum of a Bounded Below Nonempty Subset in a Subset of a Conditionally Complete Linear Order

Informal description

Let $s$ be a nonempty subset of a conditionally complete linear order $\alpha$, and let $t$ be a nonempty subset of $s$ that is bounded below in $s$. If the infimum of the image of $t$ in $\alpha$ lies within $s$, then this infimum coincides with the infimum of $t$ in the subset $s$.

subset_sInf_emptyset theorem

[Inhabited s] : sInf (∅ : Set s) = default

Full source

theorem subset_sInf_emptyset [Inhabited s] :
    sInf (∅ : Set s) = default := by
  simp [sInf]

Infimum of Empty Set in Inhabited Subset is Default Element

Informal description

For any inhabited subset $s$ of a conditionally complete linear order, the infimum of the empty set in $s$ is equal to the default element of $s$.

subset_sInf_of_not_bddBelow theorem

[Inhabited s] {t : Set s} (ht : ¬BddBelow t) : sInf t = default

Full source

theorem subset_sInf_of_not_bddBelow [Inhabited s] {t : Set s} (ht : ¬BddBelow t) :
    sInf t = default := by
  simp [sInf, ht]

Infimum of Unbounded Below Subset Equals Default Element

Informal description

Let $s$ be a nonempty subset of a type with an infimum structure. For any subset $t \subseteq s$ that is not bounded below, the infimum of $t$ in $s$ is equal to the default element of $s$.

subsetConditionallyCompleteLinearOrder abbrev

 [Inhabited s] (h_Sup : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddAbove t), sSup ((↑) '' t : Set α) ∈ s)
  (h_Inf : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddBelow t), sInf ((↑) '' t : Set α) ∈ s) :
  ConditionallyCompleteLinearOrder s

Full source

/-- For a nonempty subset of a conditionally complete linear order to be a conditionally complete
linear order, it suffices that it contain the `sSup` of all its nonempty bounded-above subsets, and
the `sInf` of all its nonempty bounded-below subsets.
See note [reducible non-instances]. -/
noncomputable abbrev subsetConditionallyCompleteLinearOrder [Inhabited s]
    (h_Sup : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddAbove t), sSupsSup ((↑) '' t : Set α) ∈ s)
    (h_Inf : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddBelow t), sInfsInf ((↑) '' t : Set α) ∈ s) :
    ConditionallyCompleteLinearOrder s :=
  { subsetSupSet s, subsetInfSet s, DistribLattice.toLattice, (inferInstance : LinearOrder s) with
    le_csSup := by
      rintro t c h_bdd hct
      rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s ⟨c, hct⟩ h_bdd (h_Sup ⟨c, hct⟩ h_bdd)]
      exact (Subtype.mono_coe _).le_csSup_image hct h_bdd
    csSup_le := by
      rintro t B ht hB
      rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s ht ⟨B, hB⟩ (h_Sup ht ⟨B, hB⟩)]
      exact (Subtype.mono_coe s).csSup_image_le ht hB
    le_csInf := by
      intro t B ht hB
      rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s ht ⟨B, hB⟩ (h_Inf ht ⟨B, hB⟩)]
      exact (Subtype.mono_coe s).le_csInf_image ht hB
    csInf_le := by
      rintro t c h_bdd hct
      rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s ⟨c, hct⟩ h_bdd (h_Inf ⟨c, hct⟩ h_bdd)]
      exact (Subtype.mono_coe s).csInf_image_le hct h_bdd
    csSup_of_not_bddAbove := fun t ht ↦ by simp [ht]
    csInf_of_not_bddBelow := fun t ht ↦ by simp [ht] }

Subset Inherits Conditionally Complete Linear Order Structure When Closed Under Suprema and Infima

Informal description

Let $s$ be a nonempty subset of a conditionally complete linear order $\alpha$. Suppose that for every nonempty subset $t \subseteq s$ that is bounded above in $s$, the supremum of $t$ in $\alpha$ lies in $s$, and similarly for every nonempty subset $t \subseteq s$ that is bounded below in $s$, the infimum of $t$ in $\alpha$ lies in $s$. Then $s$ inherits a conditionally complete linear order structure from $\alpha$.

sSup_within_of_ordConnected theorem

 {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty) (h_bdd : BddAbove t) : sSup ((↑) '' t : Set α) ∈ s

Full source

/-- The `sSup` function on a nonempty `OrdConnected` set `s` in a conditionally complete linear
order takes values within `s`, for all nonempty bounded-above subsets of `s`. -/
theorem sSup_within_of_ordConnected {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty)
    (h_bdd : BddAbove t) : sSupsSup ((↑) '' t : Set α) ∈ s := by
  obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
  obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd
  refine hs.out c.2 B.2 ⟨?_, ?_⟩
  · exact (Subtype.mono_coe s).le_csSup_image hct ⟨B, hB⟩
  · exact (Subtype.mono_coe s).csSup_image_le ⟨c, hct⟩ hB

Supremum of Bounded Above Subset in Order-Connected Set Belongs to Set

Informal description

Let $\alpha$ be a conditionally complete linear order and $s \subseteq \alpha$ be an order-connected subset. For any nonempty subset $t \subseteq s$ that is bounded above in $s$, the supremum of $t$ (computed in $\alpha$) belongs to $s$.

sInf_within_of_ordConnected theorem

 {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty) (h_bdd : BddBelow t) : sInf ((↑) '' t : Set α) ∈ s

Full source

/-- The `sInf` function on a nonempty `OrdConnected` set `s` in a conditionally complete linear
order takes values within `s`, for all nonempty bounded-below subsets of `s`. -/
theorem sInf_within_of_ordConnected {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty)
    (h_bdd : BddBelow t) : sInfsInf ((↑) '' t : Set α) ∈ s := by
  obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
  obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
  refine hs.out B.2 c.2 ⟨?_, ?_⟩
  · exact (Subtype.mono_coe s).le_csInf_image ⟨c, hct⟩ hB
  · exact (Subtype.mono_coe s).csInf_image_le hct ⟨B, hB⟩

Infimum of Bounded Below Subset in Order-Connected Set Belongs to Set

Informal description

Let $\alpha$ be a conditionally complete linear order and $s \subseteq \alpha$ be an order-connected subset. For any nonempty subset $t \subseteq s$ that is bounded below in $s$, the infimum of $t$ (computed in $\alpha$) belongs to $s$.

ordConnectedSubsetConditionallyCompleteLinearOrder instance

[Inhabited s] [OrdConnected s] : ConditionallyCompleteLinearOrder s

Full source

/-- A nonempty `OrdConnected` set in a conditionally complete linear order is naturally a
conditionally complete linear order. -/
noncomputable instance ordConnectedSubsetConditionallyCompleteLinearOrder [Inhabited s]
    [OrdConnected s] : ConditionallyCompleteLinearOrder s :=
  subsetConditionallyCompleteLinearOrder s
    (fun h => sSup_within_of_ordConnected h)
    (fun h => sInf_within_of_ordConnected h)

Order-Connected Subsets Inherit Conditionally Complete Linear Order Structure

Informal description

For any nonempty order-connected subset $s$ of a conditionally complete linear order $\alpha$, the subset $s$ inherits a conditionally complete linear order structure from $\alpha$.

Set.Icc.completeLattice instance

[ConditionallyCompleteLattice α] {a b : α} [Fact (a ≤ b)] : CompleteLattice (Set.Icc a b)

Full source

/-- Complete lattice structure on `Set.Icc` -/
noncomputable instance Set.Icc.completeLattice [ConditionallyCompleteLattice α]
    {a b : α} [Fact (a ≤ b)] : CompleteLattice (Set.Icc a b) where
  __ := (inferInstance : BoundedOrder ↑(Icc a b))
  sSup S := if hS : S = ∅ then ⟨a, le_rfl, Fact.out⟩ else ⟨sSup ((↑) '' S), by
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS
    refine ⟨?_, csSup_le (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.2)⟩
    obtain ⟨c, hc⟩ := hS
    exact c.2.1.trans (le_csSup ⟨b, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.2⟩ ⟨c, hc, rfl⟩)⟩
  le_sSup S c hc := by
    by_cases hS : S = ∅ <;> simp only [hS, dite_true, dite_false]
    · simp [hS] at hc
    · exact le_csSup ⟨b, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.2⟩ ⟨c, hc, rfl⟩
  sSup_le S c hc := by
    by_cases hS : S = ∅ <;> simp only [hS, dite_true, dite_false]
    · exact c.2.1
    · exact csSup_le ((Set.nonempty_iff_ne_empty.mpr hS).image Subtype.val)
        (fun _ ⟨d, h, hd⟩ ↦ hd ▸ hc d h)
  sInf S := if hS : S = ∅ then ⟨b, Fact.out, le_rfl⟩ else ⟨sInf ((↑) '' S), by
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS
    refine ⟨le_csInf (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.1), ?_⟩
    obtain ⟨c, hc⟩ := hS
    exact le_trans (csInf_le ⟨a, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.1⟩ ⟨c, hc, rfl⟩) c.2.2⟩
  sInf_le S c hc := by
    by_cases hS : S = ∅ <;> simp only [hS, dite_true, dite_false]
    · simp [hS] at hc
    · exact csInf_le ⟨a, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.1⟩ ⟨c, hc, rfl⟩
  le_sInf S c hc := by
    by_cases hS : S = ∅ <;> simp only [hS, dite_true, dite_false]
    · exact c.2.2
    · exact le_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image Subtype.val)
        (fun _ ⟨d, h, hd⟩ ↦ hd ▸ hc d h)

Complete Lattice Structure on Closed Intervals

Informal description

For any conditionally complete lattice $\alpha$ and elements $a, b \in \alpha$ with $a \leq b$, the closed interval $[a, b]$ forms a complete lattice. This means that every subset of $[a, b]$ has both a supremum and an infimum within $[a, b]$.

instCompleteLinearOrderElemIccOfFactLe instance

[ConditionallyCompleteLinearOrder α] {a b : α} [Fact (a ≤ b)] : CompleteLinearOrder (Set.Icc a b)

Full source

/-- Complete linear order structure on `Set.Icc` -/
noncomputable instance [ConditionallyCompleteLinearOrder α] {a b : α} [Fact (a ≤ b)] :
    CompleteLinearOrder (Set.Icc a b) :=
  { Set.Icc.completeLattice, Subtype.instLinearOrder _, LinearOrder.toBiheytingAlgebra with }

Complete Linear Order Structure on Closed Intervals

Informal description

For any conditionally complete linear order $\alpha$ and elements $a, b \in \alpha$ with $a \leq b$, the closed interval $[a, b]$ inherits a complete linear order structure from $\alpha$. This means that every subset of $[a, b]$ has both a supremum and an infimum within $[a, b]$, and the order is linear.

Set.Icc.coe_sSup theorem

 [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set (Set.Icc a b)} (hS : S.Nonempty) :
  have : Fact (a ≤ b) := ⟨h⟩
  ↑(sSup S) = sSup ((↑) '' S : Set α)

Full source

lemma Set.Icc.coe_sSup [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b)
    {S : Set (Set.Icc a b)} (hS : S.Nonempty) : have : Fact (a ≤ b) := ⟨h⟩
    ↑(sSup S) = sSup ((↑) '' S : Set α) :=
  congrArg Subtype.val (dif_neg hS.ne_empty)

Supremum in Closed Interval Equals Supremum in Ambient Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$ with $a \leq b$. For any nonempty subset $S$ of the closed interval $[a, b]$, the supremum of $S$ in $[a, b]$ (denoted $\sup S$) is equal to the supremum of the image of $S$ under the inclusion map in $\alpha$ (denoted $\sup (\iota(S))$), where $\iota : [a, b] \hookrightarrow \alpha$ is the natural inclusion. In other words, if $S \subseteq [a, b]$ is nonempty, then $\sup_{[a, b]} S = \sup_\alpha S$.

Set.Icc.coe_sInf theorem

 [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set (Set.Icc a b)} (hS : S.Nonempty) :
  have : Fact (a ≤ b) := ⟨h⟩
  ↑(sInf S) = sInf ((↑) '' S : Set α)

Full source

lemma Set.Icc.coe_sInf [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b)
    {S : Set (Set.Icc a b)} (hS : S.Nonempty) : have : Fact (a ≤ b) := ⟨h⟩
    ↑(sInf S) = sInf ((↑) '' S : Set α) :=
  congrArg Subtype.val (dif_neg hS.ne_empty)

Infimum in Closed Interval Equals Infimum in Ambient Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$ with $a \leq b$. For any nonempty subset $S$ of the closed interval $[a, b]$, the infimum of $S$ in $[a, b]$ (denoted $\inf S$) is equal to the infimum of the image of $S$ under the canonical inclusion map in $\alpha$ (denoted $\inf (\iota(S))$), where $\iota : [a, b] \hookrightarrow \alpha$ is the inclusion map.

Set.Icc.coe_iSup theorem

 [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) [Nonempty ι] {S : ι → Set.Icc a b} :
  have : Fact (a ≤ b) := ⟨h⟩
  ↑(iSup S) = (⨆ i, S i : α)

Full source

lemma Set.Icc.coe_iSup [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b)
    [Nonempty ι] {S : ι → Set.Icc a b} : have : Fact (a ≤ b) := ⟨h⟩
    ↑(iSup S) = (⨆ i, S i : α) :=
  (Set.Icc.coe_sSup h (range_nonempty S)).trans (congrArg sSup (range_comp Subtype.val S).symm)

Indexed Supremum in Closed Interval Equals Supremum in Ambient Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$ with $a \leq b$. For any nonempty index type $\iota$ and any family of elements $S : \iota \to [a, b]$, the supremum of $S$ in the closed interval $[a, b]$ (denoted $\sup_{[a, b]} S$) is equal to the supremum of $S$ in $\alpha$ (denoted $\sup_\alpha S$). In other words, if $S_i \in [a, b]$ for all $i \in \iota$, then $\sup_{i \in \iota} S_i$ computed in $[a, b]$ coincides with $\sup_{i \in \iota} S_i$ computed in $\alpha$.

Set.Icc.coe_iInf theorem

 [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) [Nonempty ι] {S : ι → Set.Icc a b} :
  have : Fact (a ≤ b) := ⟨h⟩
  ↑(iInf S) = (⨅ i, S i : α)

Full source

lemma Set.Icc.coe_iInf [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b)
    [Nonempty ι] {S : ι → Set.Icc a b} : have : Fact (a ≤ b) := ⟨h⟩
    ↑(iInf S) = (⨅ i, S i : α) :=
  (Set.Icc.coe_sInf h (range_nonempty S)).trans (congrArg sInf (range_comp Subtype.val S).symm)

Infimum in Closed Interval Equals Infimum in Ambient Lattice for Indexed Families

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$ with $a \leq b$. For any nonempty index type $\iota$ and any family of elements $S : \iota \to [a, b]$ in the closed interval $[a, b]$, the image of the infimum of $S$ under the canonical inclusion map $\iota : [a, b] \hookrightarrow \alpha$ is equal to the infimum of the family $S$ in $\alpha$, i.e., $\uparrow(\bigsqcap_i S_i) = \bigsqcap_i (S_i : \alpha)$.

Set.Iic.instCompleteLattice instance

: CompleteLattice (Iic a)

Full source

instance instCompleteLattice : CompleteLattice (Iic a) where
  sSup S := ⟨sSup ((↑) '' S), by simpa using fun b hb _ ↦ hb⟩
  sInf S := ⟨a ⊓ sInf ((↑) '' S), by simp⟩
  le_sSup _ _ hb := le_sSup <| mem_image_of_mem Subtype.val hb
  sSup_le _ _ hb := sSup_le <| fun _ ⟨c, hc, hc'⟩ ↦ hc' ▸ hb c hc
  sInf_le _ _ hb := inf_le_of_right_le <| sInf_le <| mem_image_of_mem Subtype.val hb
  le_sInf _ b hb := le_inf_iff.mpr ⟨b.property, le_sInf fun _ ⟨d, hd, hd'⟩  ↦ hd' ▸ hb d hd⟩
  le_top := by simp
  bot_le := by simp

Complete Lattice Structure on $(-\infty, a]$

Informal description

For any element $a$ in a complete lattice $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ inherits a complete lattice structure from $\alpha$.

Set.Iic.coe_sSup theorem

: (↑(sSup S) : α) = sSup ((↑) '' S)

Full source

@[simp] theorem coe_sSup : (↑(sSup S) : α) = sSup ((↑) '' S) := rfl

Supremum Commutes with Inclusion in $(-\infty, a]$

Informal description

For a set $S$ in the left-infinite right-closed interval $(-\infty, a]$ of a complete lattice $\alpha$, the image of the supremum of $S$ under the canonical inclusion map is equal to the supremum of the image of $S$ under this map. In other words, $\uparrow(\sup S) = \sup (\uparrow '' S)$.

Set.Iic.coe_iSup theorem

: (↑(⨆ i, f i) : α) = ⨆ i, (f i : α)

Full source

@[simp] theorem coe_iSup : (↑(⨆ i, f i) : α) = ⨆ i, (f i : α) := by
  rw [iSup, coe_sSup]; congr; ext; simp

Supremum Commutes with Inclusion for Indexed Family in $(-\infty, a]$

Informal description

For a left-infinite right-closed interval $(-\infty, a]$ in a complete lattice $\alpha$ and an indexed family of elements $f_i \in (-\infty, a]$, the image of the supremum $\bigsqcup_i f_i$ under the canonical inclusion map is equal to the supremum of the images of the $f_i$ in $\alpha$. That is, $\uparrow(\bigsqcup_i f_i) = \bigsqcup_i \uparrow f_i$.

Set.Iic.coe_biSup theorem

: (↑(⨆ i, ⨆ (_ : p i), f i) : α) = ⨆ i, ⨆ (_ : p i), (f i : α)

Full source

theorem coe_biSup : (↑(⨆ i, ⨆ (_ : p i), f i) : α) = ⨆ i, ⨆ (_ : p i), (f i : α) := by simp

Bounded Supremum Commutes with Inclusion in $(-\infty, a]$

Informal description

For a left-infinite right-closed interval $(-\infty, a]$ in a complete lattice $\alpha$ and a family of elements $(f_i)_{i \in \iota}$ in $(-\infty, a]$ indexed by a predicate $p$, the image of the bounded supremum $\bigsqcup_{i, p i} f_i$ under the canonical inclusion map is equal to the bounded supremum of the images of the $f_i$ in $\alpha$. That is, \[ \uparrow\left(\bigsqcup_{\substack{i \\ p i}} f_i\right) = \bigsqcup_{\substack{i \\ p i}} \uparrow f_i. \]

Set.Iic.coe_sInf theorem

: (↑(sInf S) : α) = a ⊓ sInf ((↑) '' S)

Full source

@[simp] theorem coe_sInf : (↑(sInf S) : α) = a ⊓ sInf ((↑) '' S) := rfl

Supremum in $(-\infty, a]$ as Infimum with $a$ of Supremum of Image

Informal description

For a left-infinite right-closed interval $(-\infty, a]$ in a complete lattice $\alpha$ and a subset $S \subseteq (-\infty, a]$, the supremum of $S$ in $\alpha$ is equal to the infimum of $a$ and the supremum of the image of $S$ under the inclusion map. That is, $\mathrm{sup}\, S = a \sqcap \mathrm{sup}\, \{x \mid x \in S\}$.

Set.Iic.coe_iInf theorem

: (↑(⨅ i, f i) : α) = a ⊓ ⨅ i, (f i : α)

Full source

@[simp] theorem coe_iInf : (↑(⨅ i, f i) : α) = a ⊓ ⨅ i, (f i : α) := by
  rw [iInf, coe_sInf]; congr; ext; simp

Infimum in $(-\infty, a]$ as Infimum with $a$ of Infimum of Family

Informal description

For a left-infinite right-closed interval $(-\infty, a]$ in a complete lattice $\alpha$ and an indexed family of elements $(f_i)_{i \in \iota}$ in $(-\infty, a]$, the infimum of the family in $\alpha$ is equal to the infimum of $a$ with the infimum of the family $(f_i)_{i \in \iota}$ viewed in $\alpha$. That is, \[ \left(\bigsqcap_{i} f_i\right) = a \sqcap \left(\bigsqcap_{i} f_i\right). \]

Set.Iic.coe_biInf theorem

: (↑(⨅ i, ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ i, ⨅ (_ : p i), (f i : α)

Full source

theorem coe_biInf : (↑(⨅ i, ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ i, ⨅ (_ : p i), (f i : α) := by
  cases isEmpty_or_nonempty ι
  · simp
  · simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]

Bounded Infimum Identity in $(-\infty, a]$: $\bigsqcap_{i, p_i} f_i = a \sqcap \bigsqcap_{i, p_i} f_i$

Informal description

For a left-infinite right-closed interval $(-\infty, a]$ in a complete lattice $\alpha$ and a family of elements $(f_i)_{i \in \iota}$ in $(-\infty, a]$ with predicates $(p_i)_{i \in \iota}$, the infimum of the family (taken over indices satisfying $p_i$) in $\alpha$ is equal to the infimum of $a$ with the infimum of the family $(f_i)_{i \in \iota}$ (taken over indices satisfying $p_i$) viewed in $\alpha$. That is, \[ \left(\bigsqcap_{i, p_i} f_i\right) = a \sqcap \left(\bigsqcap_{i, p_i} f_i\right). \]

TODO