Mathlib.Order.UpperLower.Principal

UpperSet.Ici definition

(a : α) : UpperSet α

Full source

/-- Principal upper set. `Set.Ici` as an upper set. The smallest upper set containing a given
element. -/
nonrec def Ici (a : α) : UpperSet α :=
  ⟨Ici a, isUpperSet_Ici a⟩

Principal upper set

Informal description

The principal upper set generated by an element $ a $ in a preorder $ \alpha $, defined as the set $ [a, \infty) $ of all elements $ x $ in $ \alpha $ such that $ a \leq x $, viewed as an upper set.

UpperSet.Ioi definition

(a : α) : UpperSet α

Full source

/-- Strict principal upper set. `Set.Ioi` as an upper set. -/
nonrec def Ioi (a : α) : UpperSet α :=
  ⟨Ioi a, isUpperSet_Ioi a⟩

Strict principal upper set

Informal description

For an element $ a $ in a preorder $ \alpha $, the strict principal upper set $ \text{Ioi}(a) $ is defined as the left-open right-infinite interval $ (a, \infty) $, consisting of all elements $ x $ in $ \alpha $ such that $ a < x $. This is represented as an upper set in the type `UpperSet α`.

UpperSet.coe_Ici theorem

(a : α) : ↑(Ici a) = Set.Ici a

Full source

@[simp]
theorem coe_Ici (a : α) : ↑(Ici a) = Set.Ici a :=
  rfl

Equality of Principal Upper Set and Interval $[a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the carrier set of the principal upper set $\text{Ici}(a)$ is equal to the left-closed right-infinite interval $[a, \infty)$. In other words, the underlying set of $\text{Ici}(a)$ is precisely $\{x \in \alpha \mid a \leq x\}$.

UpperSet.coe_Ioi theorem

(a : α) : ↑(Ioi a) = Set.Ioi a

Full source

@[simp]
theorem coe_Ioi (a : α) : ↑(Ioi a) = Set.Ioi a :=
  rfl

Equality of Strict Principal Upper Set and Interval $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the carrier set of the strict principal upper set $\text{Ioi}(a)$ is equal to the left-open right-infinite interval $(a, \infty)$. In other words, the underlying set of $\text{Ioi}(a)$ is precisely $\{x \in \alpha \mid a < x\}$.

UpperSet.mem_Ici_iff theorem

: b ∈ Ici a ↔ a ≤ b

Full source

@[simp]
theorem mem_Ici_iff : b ∈ Ici ab ∈ Ici a ↔ a ≤ b :=
  Iff.rfl

Membership Criterion for Principal Upper Set: $b \in [a, \infty) \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the element $b$ belongs to the principal upper set $\text{Ici}(a)$ if and only if $a \leq b$.

UpperSet.mem_Ioi_iff theorem

: b ∈ Ioi a ↔ a < b

Full source

@[simp]
theorem mem_Ioi_iff : b ∈ Ioi ab ∈ Ioi a ↔ a < b :=
  Iff.rfl

Membership Criterion for Strict Principal Upper Set: $b \in \text{Ioi}(a) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the element $b$ belongs to the strict principal upper set $\text{Ioi}(a)$ if and only if $a < b$.

UpperSet.map_Ici theorem

(f : α ≃o β) (a : α) : map f (Ici a) = Ici (f a)

Full source

@[simp]
theorem map_Ici (f : α ≃o β) (a : α) : map f (Ici a) = Ici (f a) := by
  ext
  simp

Image of Principal Upper Set under Order Isomorphism: $f([a, \infty)) = [f(a), \infty)$

Informal description

Let $f : \alpha \simeqo \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the principal upper set $[a, \infty)$ under the upper set map induced by $f$ equals the principal upper set $[f(a), \infty)$ in $\beta$. That is, $$ f\big( [a, \infty) \big) = [f(a), \infty). $$

UpperSet.map_Ioi theorem

(f : α ≃o β) (a : α) : map f (Ioi a) = Ioi (f a)

Full source

@[simp]
theorem map_Ioi (f : α ≃o β) (a : α) : map f (Ioi a) = Ioi (f a) := by
  ext
  simp

Image of Strict Principal Upper Set under Order Isomorphism

Informal description

Let $f : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the strict principal upper set $(a, \infty)$ under the upper set map induced by $f$ is equal to the strict principal upper set $(f(a), \infty)$ in $\beta$. In other words: $$ f\big( (a, \infty) \big) = (f(a), \infty) $$

UpperSet.Ici_le_Ioi theorem

(a : α) : Ici a ≤ Ioi a

Full source

theorem Ici_le_Ioi (a : α) : Ici a ≤ Ioi a :=
  Ioi_subset_Ici_self

Inclusion of Principal Upper Sets: $[a, \infty) \subseteq (a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the principal upper set $[a, \infty)$ is less than or equal to the strict principal upper set $(a, \infty)$ in the lattice of upper sets ordered by reverse inclusion.

UpperSet.Ici_bot theorem

[OrderBot α] : Ici (⊥ : α) = ⊥

Full source

@[simp]
nonrec theorem Ici_bot [OrderBot α] : Ici (⊥ : α) = ⊥ :=
  SetLike.coe_injective Ici_bot

Principal Upper Set at Bottom is Bottom Element

Informal description

In a preorder $\alpha$ with a bottom element $\bot$, the principal upper set $[\bot, \infty)$ is equal to the bottom element $\bot$ of the lattice of upper sets ordered by reverse inclusion.

UpperSet.Ioi_top theorem

[OrderTop α] : Ioi (⊤ : α) = ⊤

Full source

@[simp]
nonrec theorem Ioi_top [OrderTop α] : Ioi (⊤ : α) = ⊤ :=
  SetLike.coe_injective Ioi_top

Strict Upper Set at Top is Greatest Upper Set: $(⊤, \infty) = ⊤$

Informal description

For any type $\alpha$ with a preorder and a greatest element $\top$, the strict principal upper set $(⊤, \infty)$ is equal to the greatest upper set $\top$ in the lattice of upper sets ordered by reverse inclusion.

UpperSet.Ici_ne_top theorem

: Ici a ≠ ⊤

Full source

@[simp] lemma Ici_ne_top : IciIci a ≠ ⊤ := SetLike.coe_ne_coe.1 nonempty_Ici.ne_empty

Principal Upper Set is Not the Greatest Upper Set

Informal description

For any element $a$ in a preorder $\alpha$, the principal upper set $[a, \infty)$ is not equal to the greatest upper set $\top$.

UpperSet.Ici_lt_top theorem

: Ici a < ⊤

Full source

@[simp] lemma Ici_lt_top : Ici a < ⊤ := lt_top_iff_ne_top.2 Ici_ne_top

Principal Upper Set is Strictly Below Top: $[a, \infty) < \top$

Informal description

For any element $a$ in a preorder $\alpha$, the principal upper set $[a, \infty)$ is strictly less than the greatest upper set $\top$ in the reverse inclusion order of upper sets.

UpperSet.le_Ici theorem

: s ≤ Ici a ↔ a ∈ s

Full source

@[simp] lemma le_Ici : s ≤ Ici a ↔ a ∈ s := ⟨fun h ↦ h le_rfl, fun ha ↦ s.upper.Ici_subset ha⟩

Characterization of Upper Set Containment in Principal Upper Set

Informal description

For any upper set $s$ in a preorder $\alpha$ and any element $a \in \alpha$, the upper set $s$ is contained in the principal upper set $[a, \infty)$ if and only if $a$ belongs to $s$.

UpperSet.Ici_injective theorem

: Injective (Ici : α → UpperSet α)

Full source

nonrec lemma Ici_injective : Injective (Ici : α → UpperSet α) := fun _a _b hab ↦
  Ici_injective <| congr_arg ((↑) : _ → Set α) hab

Injectivity of the Principal Upper Set Construction

Informal description

The function that maps each element $a$ in a preorder $\alpha$ to the principal upper set $[a, \infty)$ is injective. That is, for any two elements $a, b \in \alpha$, if $[a, \infty) = [b, \infty)$ as upper sets, then $a = b$.

UpperSet.Ici_inj theorem

: Ici a = Ici b ↔ a = b

Full source

@[simp] lemma Ici_inj : IciIci a = Ici b ↔ a = b := Ici_injective.eq_iff

Equality of Principal Upper Sets Characterizes Element Equality

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the principal upper sets $[a, \infty)$ and $[b, \infty)$ are equal if and only if $a = b$.

UpperSet.Ici_ne_Ici theorem

: Ici a ≠ Ici b ↔ a ≠ b

Full source

lemma Ici_ne_Ici : IciIci a ≠ Ici bIci a ≠ Ici b ↔ a ≠ b := Ici_inj.not

Inequality of Principal Upper Sets Characterizes Element Inequality

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the principal upper sets $[a, \infty)$ and $[b, \infty)$ are not equal if and only if $a \neq b$.

UpperSet.Ici_sup theorem

[SemilatticeSup α] (a b : α) : Ici (a ⊔ b) = Ici a ⊔ Ici b

Full source

@[simp]
theorem Ici_sup [SemilatticeSup α] (a b : α) : Ici (a ⊔ b) = IciIci a ⊔ Ici b :=
  ext Ici_inter_Ici.symm

Supremum of Principal Upper Sets Equals Principal Upper Set of Supremum

Informal description

Let $\alpha$ be a semilattice with a supremum operation $\sqcup$. For any elements $a, b \in \alpha$, the principal upper set generated by $a \sqcup b$ is equal to the supremum of the principal upper sets generated by $a$ and $b$. In other words, $$[a \sqcup b, \infty) = [a, \infty) \sqcup [b, \infty).$$

UpperSet.Ici_sSup theorem

(S : Set α) : Ici (sSup S) = ⨆ a ∈ S, Ici a

Full source

@[simp]
theorem Ici_sSup (S : Set α) : Ici (sSup S) = ⨆ a ∈ S, Ici a :=
  SetLike.ext fun c => by simp only [mem_Ici_iff, mem_iSup_iff, sSup_le_iff]

Supremum of Principal Upper Sets Equals Principal Upper Set of Supremum

Informal description

For any subset $S$ of a complete lattice $\alpha$, the principal upper set generated by the supremum of $S$ is equal to the supremum of the family of principal upper sets generated by each element of $S$. In other words, $[ \sup S, \infty ) = \bigsqcup_{a \in S} [a, \infty)$.

UpperSet.Ici_iSup theorem

(f : ι → α) : Ici (⨆ i, f i) = ⨆ i, Ici (f i)

Full source

@[simp]
theorem Ici_iSup (f : ι → α) : Ici (⨆ i, f i) = ⨆ i, Ici (f i) :=
  SetLike.ext fun c => by simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

Supremum of Principal Upper Sets Equals Principal Upper Set of Supremum

Informal description

For any family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$, the principal upper set generated by their supremum $\bigsqcup_i f_i$ is equal to the supremum of the principal upper sets generated by each $f_i$. That is, $$[\bigsqcup_i f_i, \infty) = \bigsqcup_i [f_i, \infty).$$

UpperSet.Ici_iSup₂ theorem

(f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⨆ (i) (j), Ici (f i j)

Full source

theorem Ici_iSup₂ (f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⨆ (i) (j), Ici (f i j) := by
  simp

Supremum of Doubly-Indexed Principal Upper Sets Equals Principal Upper Set of Supremum

Informal description

For any doubly-indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in a complete lattice $\alpha$, the principal upper set generated by their supremum $\bigsqcup_{i,j} f_{i,j}$ is equal to the supremum of the principal upper sets generated by each $f_{i,j}$. That is, $$[\bigsqcup_{i,j} f_{i,j}, \infty) = \bigsqcup_{i,j} [f_{i,j}, \infty).$$

LowerSet.Iic definition

(a : α) : LowerSet α

Full source

/-- Principal lower set. `Set.Iic` as a lower set. The smallest lower set containing a given
element. -/
nonrec def Iic (a : α) : LowerSet α :=
  ⟨Iic a, isLowerSet_Iic a⟩

Principal lower set $ (-\infty, a] $

Informal description

For an element $ a $ in a preorder $ \alpha $, the principal lower set $ \text{Iic } a $ is defined as the left-infinite right-closed interval $ (-\infty, a] $, consisting of all elements $ x $ in $ \alpha $ such that $ x \leq a $. This is the smallest lower set containing $ a $.

LowerSet.Iio definition

(a : α) : LowerSet α

Full source

/-- Strict principal lower set. `Set.Iio` as a lower set. -/
nonrec def Iio (a : α) : LowerSet α :=
  ⟨Iio a, isLowerSet_Iio a⟩

Strict principal lower set $\operatorname{Iio}(a)$

Informal description

For an element $a$ in a preorder $\alpha$, the strict principal lower set $\operatorname{Iio}(a)$ is defined as the lower set consisting of all elements less than $a$, i.e., $\{x \mid x < a\}$.

LowerSet.coe_Iic theorem

(a : α) : ↑(Iic a) = Set.Iic a

Full source

@[simp]
theorem coe_Iic (a : α) : ↑(Iic a) = Set.Iic a :=
  rfl

Principal Lower Set Equals Interval $(-\infty, a]$

Informal description

For any element $a$ in a preorder $\alpha$, the underlying set of the principal lower set $\operatorname{Iic}(a)$ is equal to the left-infinite right-closed interval $(-\infty, a]$, i.e., $\operatorname{Iic}(a) = \{x \mid x \leq a\}$.

LowerSet.coe_Iio theorem

(a : α) : ↑(Iio a) = Set.Iio a

Full source

@[simp]
theorem coe_Iio (a : α) : ↑(Iio a) = Set.Iio a :=
  rfl

Strict Principal Lower Set Equals Interval $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the underlying set of the strict principal lower set $\operatorname{Iio}(a)$ is equal to the left-infinite right-open interval $(-\infty, a)$, i.e., $\operatorname{Iio}(a) = \{x \mid x < a\}$.

LowerSet.mem_Iic_iff theorem

: b ∈ Iic a ↔ b ≤ a

Full source

@[simp]
theorem mem_Iic_iff : b ∈ Iic ab ∈ Iic a ↔ b ≤ a :=
  Iff.rfl

Membership Criterion for Principal Lower Set: $b \in (-\infty, a] \leftrightarrow b \leq a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the element $b$ belongs to the principal lower set $\operatorname{Iic}(a)$ if and only if $b \leq a$.

LowerSet.mem_Iio_iff theorem

: b ∈ Iio a ↔ b < a

Full source

@[simp]
theorem mem_Iio_iff : b ∈ Iio ab ∈ Iio a ↔ b < a :=
  Iff.rfl

Membership Criterion for Strict Principal Lower Set: $b \in (-\infty, a) \leftrightarrow b < a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the element $b$ belongs to the strict principal lower set $\operatorname{Iio}(a)$ if and only if $b < a$.

LowerSet.map_Iic theorem

(f : α ≃o β) (a : α) : map f (Iic a) = Iic (f a)

Full source

@[simp]
theorem map_Iic (f : α ≃o β) (a : α) : map f (Iic a) = Iic (f a) := by
  ext
  simp

Image of Principal Lower Set under Order Isomorphism: $f((-\infty, a]) = (-\infty, f(a)]$

Informal description

Let $f : \alpha \simeq \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the principal lower set $(-\infty, a]$ under the map induced by $f$ is equal to the principal lower set $(-\infty, f(a)]$ in $\beta$. That is, $$ f\big( (-\infty, a] \big) = (-\infty, f(a)]. $$

LowerSet.map_Iio theorem

(f : α ≃o β) (a : α) : map f (Iio a) = Iio (f a)

Full source

@[simp]
theorem map_Iio (f : α ≃o β) (a : α) : map f (Iio a) = Iio (f a) := by
  ext
  simp

Image of Strict Principal Lower Set under Order Isomorphism: $f(\operatorname{Iio}(a)) = \operatorname{Iio}(f(a))$

Informal description

Let $f : \alpha \simeq \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the strict principal lower set $\operatorname{Iio}(a) = \{x \mid x < a\}$ under $f$ is equal to the strict principal lower set $\operatorname{Iio}(f(a))$ in $\beta$. That is: $$ f(\operatorname{Iio}(a)) = \operatorname{Iio}(f(a)) $$

LowerSet.Ioi_le_Ici theorem

(a : α) : Ioi a ≤ Ici a

Full source

theorem Ioi_le_Ici (a : α) : Ioi a ≤ Ici a :=
  Ioi_subset_Ici_self

Order Relation Between Open and Closed Right-Infinite Intervals: $(a, \infty) \leq [a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a, \infty)$ is less than or equal to the left-closed right-infinite interval $[a, \infty)$ in the order of lower sets.

LowerSet.Iic_top theorem

[OrderTop α] : Iic (⊤ : α) = ⊤

Full source

@[simp]
nonrec theorem Iic_top [OrderTop α] : Iic (⊤ : α) = ⊤ :=
  SetLike.coe_injective Iic_top

Principal Lower Set at Top Equals Entire Set

Informal description

In a partially ordered set $\alpha$ with a greatest element $\top$, the principal lower set $(-\infty, \top]$ is equal to the entire set $\alpha$ (i.e., the top element in the lattice of lower sets).

LowerSet.Iio_bot theorem

[OrderBot α] : Iio (⊥ : α) = ⊥

Full source

@[simp]
nonrec theorem Iio_bot [OrderBot α] : Iio (⊥ : α) = ⊥ :=
  SetLike.coe_injective Iio_bot

Strict Lower Set Below Bottom Equals Bottom Element: $\operatorname{Iio}(\bot) = \bot$

Informal description

In an ordered type $\alpha$ with a bottom element $\bot$, the strict principal lower set $\{x \mid x < \bot\}$ is equal to the bottom element of the lattice of lower sets.

LowerSet.Iic_ne_bot theorem

: Iic a ≠ ⊥

Full source

@[simp] lemma Iic_ne_bot : IicIic a ≠ ⊥ := SetLike.coe_ne_coe.1 nonempty_Iic.ne_empty

Non-triviality of principal lower sets: $(-\infty, a] \neq \bot$

Informal description

For any element $a$ in a preorder $\alpha$, the principal lower set $(-\infty, a]$ is not equal to the bottom element of the lattice of lower sets.

LowerSet.bot_lt_Iic theorem

: ⊥ < Iic a

Full source

@[simp] lemma bot_lt_Iic : ⊥ < Iic a := bot_lt_iff_ne_bot.2 Iic_ne_bot

Strict Inequality: $\bot < (-\infty, a]$ in Lower Sets Lattice

Informal description

For any element $a$ in a preorder $\alpha$, the bottom element $\bot$ of the lattice of lower sets is strictly less than the principal lower set $(-\infty, a]$.

LowerSet.Iic_le theorem

: Iic a ≤ s ↔ a ∈ s

Full source

@[simp] lemma Iic_le : IicIic a ≤ s ↔ a ∈ s := ⟨fun h ↦ h le_rfl, fun ha ↦ s.lower.Iic_subset ha⟩

Principal Lower Set Containment Criterion: $(-\infty, a] \leq s \leftrightarrow a \in s$

Informal description

For any element $a$ in a preorder $\alpha$ and any lower set $s$ of $\alpha$, the principal lower set $(-\infty, a]$ is contained in $s$ if and only if $a$ belongs to $s$.

LowerSet.Iic_injective theorem

: Injective (Iic : α → LowerSet α)

Full source

nonrec lemma Iic_injective : Injective (Iic : α → LowerSet α) := fun _a _b hab ↦
  Iic_injective <| congr_arg ((↑) : _ → Set α) hab

Injectivity of Principal Lower Set Construction

Informal description

The function that maps each element $a$ in a preorder $\alpha$ to the principal lower set $(-\infty, a]$ is injective. In other words, if $(-\infty, a] = (-\infty, b]$ as lower sets, then $a = b$.

LowerSet.Iic_inj theorem

: Iic a = Iic b ↔ a = b

Full source

@[simp] lemma Iic_inj : IicIic a = Iic b ↔ a = b := Iic_injective.eq_iff

Equality of Principal Lower Sets Characterizes Element Equality

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the principal lower sets $(-\infty, a]$ and $(-\infty, b]$ are equal if and only if $a = b$.

LowerSet.Iic_ne_Iic theorem

: Iic a ≠ Iic b ↔ a ≠ b

Full source

lemma Iic_ne_Iic : IicIic a ≠ Iic bIic a ≠ Iic b ↔ a ≠ b := Iic_inj.not

Inequality of Principal Lower Sets Characterizes Element Inequality

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the principal lower sets $(-\infty, a]$ and $(-\infty, b]$ are not equal if and only if $a \neq b$.

LowerSet.Iic_inf theorem

[SemilatticeInf α] (a b : α) : Iic (a ⊓ b) = Iic a ⊓ Iic b

Full source

@[simp]
theorem Iic_inf [SemilatticeInf α] (a b : α) : Iic (a ⊓ b) = IicIic a ⊓ Iic b :=
  SetLike.coe_injective Iic_inter_Iic.symm

Principal Lower Set of Infimum Equals Infimum of Principal Lower Sets

Informal description

Let $\alpha$ be a semilattice with infima. For any elements $a, b \in \alpha$, the principal lower set generated by the infimum $a \sqcap b$ is equal to the infimum of the principal lower sets generated by $a$ and $b$. In symbols: \[ \text{Iic}(a \sqcap b) = \text{Iic}(a) \sqcap \text{Iic}(b). \]

LowerSet.Iic_sInf theorem

(S : Set α) : Iic (sInf S) = ⨅ a ∈ S, Iic a

Full source

@[simp]
theorem Iic_sInf (S : Set α) : Iic (sInf S) = ⨅ a ∈ S, Iic a :=
  SetLike.ext fun c => by simp only [mem_Iic_iff, mem_iInf₂_iff, le_sInf_iff]

Principal Lower Set of Infimum Equals Infimum of Principal Lower Sets

Informal description

For any subset $S$ of a complete lattice $\alpha$, the principal lower set generated by the infimum of $S$ is equal to the infimum of the principal lower sets generated by each element $a \in S$. In symbols: \[ \text{Iic}\left(\bigwedge S\right) = \bigwedge_{a \in S} \text{Iic}(a). \]

LowerSet.Iic_iInf theorem

(f : ι → α) : Iic (⨅ i, f i) = ⨅ i, Iic (f i)

Full source

@[simp]
theorem Iic_iInf (f : ι → α) : Iic (⨅ i, f i) = ⨅ i, Iic (f i) :=
  SetLike.ext fun c => by simp only [mem_Iic_iff, mem_iInf_iff, le_iInf_iff]

Principal Lower Set of Infimum Equals Infimum of Principal Lower Sets

Informal description

For any family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$, the principal lower set generated by the infimum of the family is equal to the infimum of the principal lower sets generated by each element $f_i$. In symbols: \[ \text{Iic}\left(\bigwedge_{i} f_i\right) = \bigwedge_{i} \text{Iic}(f_i). \]

LowerSet.Iic_iInf₂ theorem

(f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⨅ (i) (j), Iic (f i j)

Full source

theorem Iic_iInf₂ (f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⨅ (i) (j), Iic (f i j) := by
  simp

Principal Lower Set of Double Infimum Equals Double Infimum of Principal Lower Sets

Informal description

For any family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in a complete lattice $\alpha$, the principal lower set generated by the infimum of the family is equal to the infimum of the principal lower sets generated by each element $f_{i,j}$. In symbols: \[ \text{Iic}\left(\bigwedge_{i,j} f_{i,j}\right) = \bigwedge_{i,j} \text{Iic}(f_{i,j}). \]

Main declarations