mathlib documentation

order.upper_lower

Up-sets and down-sets #

This file defines upper and lower sets in an order.

Main declarations #

TODO #

Lattice structure on antichains. Order equivalence between upper/lower sets and antichains.

Unbundled upper/lower sets #

def is_upper_set {α : Type u_1} [has_le α] (s : set α) :
Prop

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

Equations
def is_lower_set {α : Type u_1} [has_le α] (s : set α) :
Prop

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

Equations
theorem is_upper_set_empty {α : Type u_1} [has_le α] :
theorem is_lower_set_empty {α : Type u_1} [has_le α] :
theorem is_upper_set_univ {α : Type u_1} [has_le α] :
theorem is_lower_set_univ {α : Type u_1} [has_le α] :
theorem is_upper_set.compl {α : Type u_1} [has_le α] {s : set α} (hs : is_upper_set s) :
theorem is_lower_set.compl {α : Type u_1} [has_le α] {s : set α} (hs : is_lower_set s) :
theorem is_upper_set.union {α : Type u_1} [has_le α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
theorem is_lower_set.union {α : Type u_1} [has_le α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
theorem is_upper_set.inter {α : Type u_1} [has_le α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
theorem is_lower_set.inter {α : Type u_1} [has_le α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
theorem is_upper_set_Union {α : Type u_1} {ι : Sort u_2} [has_le α] {f : ι → set α} (hf : ∀ (i : ι), is_upper_set (f i)) :
is_upper_set (⋃ (i : ι), f i)
theorem is_lower_set_Union {α : Type u_1} {ι : Sort u_2} [has_le α] {f : ι → set α} (hf : ∀ (i : ι), is_lower_set (f i)) :
is_lower_set (⋃ (i : ι), f i)
theorem is_upper_set_Union₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {f : Π (i : ι), κ iset α} (hf : ∀ (i : ι) (j : κ i), is_upper_set (f i j)) :
is_upper_set (⋃ (i : ι) (j : κ i), f i j)
theorem is_lower_set_Union₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {f : Π (i : ι), κ iset α} (hf : ∀ (i : ι) (j : κ i), is_lower_set (f i j)) :
is_lower_set (⋃ (i : ι) (j : κ i), f i j)
theorem is_upper_set_sUnion {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s Sis_upper_set s) :
theorem is_lower_set_sUnion {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s Sis_lower_set s) :
theorem is_upper_set_Inter {α : Type u_1} {ι : Sort u_2} [has_le α] {f : ι → set α} (hf : ∀ (i : ι), is_upper_set (f i)) :
is_upper_set (⋂ (i : ι), f i)
theorem is_lower_set_Inter {α : Type u_1} {ι : Sort u_2} [has_le α] {f : ι → set α} (hf : ∀ (i : ι), is_lower_set (f i)) :
is_lower_set (⋂ (i : ι), f i)
theorem is_upper_set_Inter₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {f : Π (i : ι), κ iset α} (hf : ∀ (i : ι) (j : κ i), is_upper_set (f i j)) :
is_upper_set (⋂ (i : ι) (j : κ i), f i j)
theorem is_lower_set_Inter₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {f : Π (i : ι), κ iset α} (hf : ∀ (i : ι) (j : κ i), is_lower_set (f i j)) :
is_lower_set (⋂ (i : ι) (j : κ i), f i j)
theorem is_upper_set_sInter {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s Sis_upper_set s) :
theorem is_lower_set_sInter {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s Sis_lower_set s) :
theorem is_upper_set.of_dual {α : Type u_1} [has_le α] {s : set α} :

Alias of the reverse direction of is_lower_set_preimage_of_dual_iff`.

theorem is_lower_set.of_dual {α : Type u_1} [has_le α] {s : set α} :

Alias of the reverse direction of is_upper_set_preimage_of_dual_iff`.

theorem is_upper_set.to_dual {α : Type u_1} [has_le α] {s : set αᵒᵈ} :

Alias of the reverse direction of is_lower_set_preimage_to_dual_iff`.

theorem is_lower_set.to_dual {α : Type u_1} [has_le α] {s : set αᵒᵈ} :

Alias of the reverse direction of is_upper_set_preimage_to_dual_iff`.

theorem is_upper_set_Ici {α : Type u_1} [preorder α] (a : α) :
theorem is_lower_set_Iic {α : Type u_1} [preorder α] (a : α) :
theorem is_upper_set_Ioi {α : Type u_1} [preorder α] (a : α) :
theorem is_lower_set_Iio {α : Type u_1} [preorder α] (a : α) :

Bundled upper/lower sets #

structure upper_set (α : Type u_4) [has_le α] :
Type u_4

The type of upper sets of an order.

Instances for upper_set
structure lower_set (α : Type u_4) [has_le α] :
Type u_4

The type of lower sets of an order.

Instances for lower_set
@[protected, instance]
def upper_set.set_like {α : Type u_1} [has_le α] :
Equations
@[ext]
theorem upper_set.ext {α : Type u_1} [has_le α] {s t : upper_set α} :
s = ts = t
@[simp]
theorem upper_set.carrier_eq_coe {α : Type u_1} [has_le α] (s : upper_set α) :
@[protected]
theorem upper_set.upper {α : Type u_1} [has_le α] (s : upper_set α) :
@[protected, instance]
def lower_set.set_like {α : Type u_1} [has_le α] :
Equations
@[ext]
theorem lower_set.ext {α : Type u_1} [has_le α] {s t : lower_set α} :
s = ts = t
@[simp]
theorem lower_set.carrier_eq_coe {α : Type u_1} [has_le α] (s : lower_set α) :
@[protected]
theorem lower_set.lower {α : Type u_1} [has_le α] (s : lower_set α) :

Order #

@[protected, instance]
def upper_set.has_sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_top {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_bot {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_Sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_Inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def upper_set.inhabited {α : Type u_1} [has_le α] :
Equations
@[simp]
theorem upper_set.coe_top {α : Type u_1} [has_le α] :
@[simp]
theorem upper_set.coe_bot {α : Type u_1} [has_le α] :
@[simp]
theorem upper_set.coe_sup {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t) = s t
@[simp]
theorem upper_set.coe_inf {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t) = s t
@[simp]
theorem upper_set.coe_Sup {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Sup.Sup S) = ⋃ (s : upper_set α) (H : s S), s
@[simp]
theorem upper_set.coe_Inf {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Inf.Inf S) = ⋂ (s : upper_set α) (H : s S), s
@[simp]
theorem upper_set.coe_supr {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → upper_set α) :
(⨆ (i : ι), f i) = ⋃ (i : ι), (f i)
@[simp]
theorem upper_set.coe_infi {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → upper_set α) :
(⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
@[simp]
theorem upper_set.coe_supr₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ iupper_set α) :
(⨆ (i : ι) (j : κ i), f i j) = ⋃ (i : ι) (j : κ i), (f i j)
@[simp]
theorem upper_set.coe_infi₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ iupper_set α) :
(⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), (f i j)
@[simp]
theorem upper_set.mem_top {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem upper_set.not_mem_bot {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem upper_set.mem_sup_iff {α : Type u_1} [has_le α] {s t : upper_set α} {a : α} :
a s t a s a t
@[simp]
theorem upper_set.mem_inf_iff {α : Type u_1} [has_le α] {s t : upper_set α} {a : α} :
a s t a s a t
@[simp]
theorem upper_set.mem_Sup_iff {α : Type u_1} [has_le α] {S : set (upper_set α)} {a : α} :
a has_Sup.Sup S ∃ (s : upper_set α) (H : s S), a s
@[simp]
theorem upper_set.mem_Inf_iff {α : Type u_1} [has_le α] {S : set (upper_set α)} {a : α} :
a has_Inf.Inf S ∀ (s : upper_set α), s Sa s
@[simp]
theorem upper_set.mem_supr_iff {α : Type u_1} {ι : Sort u_2} [has_le α] {a : α} {f : ι → upper_set α} :
(a ⨆ (i : ι), f i) ∃ (i : ι), a f i
@[simp]
theorem upper_set.mem_infi_iff {α : Type u_1} {ι : Sort u_2} [has_le α] {a : α} {f : ι → upper_set α} :
(a ⨅ (i : ι), f i) ∀ (i : ι), a f i
@[simp]
theorem upper_set.mem_supr₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {a : α} {f : Π (i : ι), κ iupper_set α} :
(a ⨆ (i : ι) (j : κ i), f i j) ∃ (i : ι) (j : κ i), a f i j
@[simp]
theorem upper_set.mem_infi₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {a : α} {f : Π (i : ι), κ iupper_set α} :
(a ⨅ (i : ι) (j : κ i), f i j) ∀ (i : ι) (j : κ i), a f i j
@[protected, instance]
def lower_set.has_sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_top {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_bot {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_Sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_Inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def lower_set.inhabited {α : Type u_1} [has_le α] :
Equations
@[simp]
theorem lower_set.coe_top {α : Type u_1} [has_le α] :
@[simp]
theorem lower_set.coe_bot {α : Type u_1} [has_le α] :
@[simp]
theorem lower_set.coe_sup {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t) = s t
@[simp]
theorem lower_set.coe_inf {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t) = s t
@[simp]
theorem lower_set.coe_Sup {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Sup.Sup S) = ⋃ (s : lower_set α) (H : s S), s
@[simp]
theorem lower_set.coe_Inf {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Inf.Inf S) = ⋂ (s : lower_set α) (H : s S), s
@[simp]
theorem lower_set.coe_supr {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → lower_set α) :
(⨆ (i : ι), f i) = ⋃ (i : ι), (f i)
@[simp]
theorem lower_set.coe_infi {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → lower_set α) :
(⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
@[simp]
theorem lower_set.coe_supr₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ ilower_set α) :
(⨆ (i : ι) (j : κ i), f i j) = ⋃ (i : ι) (j : κ i), (f i j)
@[simp]
theorem lower_set.coe_infi₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ ilower_set α) :
(⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), (f i j)
@[simp]
theorem lower_set.mem_top {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem lower_set.not_mem_bot {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem lower_set.mem_sup_iff {α : Type u_1} [has_le α] {s t : lower_set α} {a : α} :
a s t a s a t
@[simp]
theorem lower_set.mem_inf_iff {α : Type u_1} [has_le α] {s t : lower_set α} {a : α} :
a s t a s a t
@[simp]
theorem lower_set.mem_Sup_iff {α : Type u_1} [has_le α] {S : set (lower_set α)} {a : α} :
a has_Sup.Sup S ∃ (s : lower_set α) (H : s S), a s
@[simp]
theorem lower_set.mem_Inf_iff {α : Type u_1} [has_le α] {S : set (lower_set α)} {a : α} :
a has_Inf.Inf S ∀ (s : lower_set α), s Sa s
@[simp]
theorem lower_set.mem_supr_iff {α : Type u_1} {ι : Sort u_2} [has_le α] {a : α} {f : ι → lower_set α} :
(a ⨆ (i : ι), f i) ∃ (i : ι), a f i
@[simp]
theorem lower_set.mem_infi_iff {α : Type u_1} {ι : Sort u_2} [has_le α] {a : α} {f : ι → lower_set α} :
(a ⨅ (i : ι), f i) ∀ (i : ι), a f i
@[simp]
theorem lower_set.mem_supr₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {a : α} {f : Π (i : ι), κ ilower_set α} :
(a ⨆ (i : ι) (j : κ i), f i j) ∃ (i : ι) (j : κ i), a f i j
@[simp]
theorem lower_set.mem_infi₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] {a : α} {f : Π (i : ι), κ ilower_set α} :
(a ⨅ (i : ι) (j : κ i), f i j) ∀ (i : ι) (j : κ i), a f i j

Complement #

def upper_set.compl {α : Type u_1} [has_le α] (s : upper_set α) :

The complement of a lower set as an upper set.

Equations
def lower_set.compl {α : Type u_1} [has_le α] (s : lower_set α) :

The complement of a lower set as an upper set.

Equations
@[simp]
theorem upper_set.coe_compl {α : Type u_1} [has_le α] (s : upper_set α) :
@[simp]
theorem upper_set.mem_compl_iff {α : Type u_1} [has_le α] {s : upper_set α} {a : α} :
a s.compl a s
@[simp]
theorem upper_set.compl_compl {α : Type u_1} [has_le α] (s : upper_set α) :
@[protected, simp]
theorem upper_set.compl_sup {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t).compl = s.compl t.compl
@[protected, simp]
theorem upper_set.compl_inf {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t).compl = s.compl t.compl
@[protected, simp]
theorem upper_set.compl_top {α : Type u_1} [has_le α] :
@[protected, simp]
theorem upper_set.compl_bot {α : Type u_1} [has_le α] :
@[protected, simp]
theorem upper_set.compl_Sup {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Sup.Sup S).compl = ⨅ (s : upper_set α) (H : s S), s.compl
@[protected, simp]
theorem upper_set.compl_Inf {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Inf.Inf S).compl = ⨆ (s : upper_set α) (H : s S), s.compl
@[protected, simp]
theorem upper_set.compl_supr {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → upper_set α) :
(⨆ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
@[protected, simp]
theorem upper_set.compl_infi {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → upper_set α) :
(⨅ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
@[simp]
theorem upper_set.compl_supr₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ iupper_set α) :
(⨆ (i : ι) (j : κ i), f i j).compl = ⨅ (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem upper_set.compl_infi₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ iupper_set α) :
(⨅ (i : ι) (j : κ i), f i j).compl = ⨆ (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem lower_set.coe_compl {α : Type u_1} [has_le α] (s : lower_set α) :
@[simp]
theorem lower_set.mem_compl_iff {α : Type u_1} [has_le α] {s : lower_set α} {a : α} :
a s.compl a s
@[simp]
theorem lower_set.compl_compl {α : Type u_1} [has_le α] (s : lower_set α) :
@[protected]
theorem lower_set.compl_sup {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t).compl = s.compl t.compl
@[protected]
theorem lower_set.compl_inf {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t).compl = s.compl t.compl
@[protected]
theorem lower_set.compl_top {α : Type u_1} [has_le α] :
@[protected]
theorem lower_set.compl_bot {α : Type u_1} [has_le α] :
@[protected]
theorem lower_set.compl_Sup {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Sup.Sup S).compl = ⨅ (s : lower_set α) (H : s S), s.compl
@[protected]
theorem lower_set.compl_Inf {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Inf.Inf S).compl = ⨆ (s : lower_set α) (H : s S), s.compl
@[protected]
theorem lower_set.compl_supr {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → lower_set α) :
(⨆ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
@[protected]
theorem lower_set.compl_infi {α : Type u_1} {ι : Sort u_2} [has_le α] (f : ι → lower_set α) :
(⨅ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
@[simp]
theorem lower_set.compl_supr₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ ilower_set α) :
(⨆ (i : ι) (j : κ i), f i j).compl = ⨅ (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem lower_set.compl_infi₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [has_le α] (f : Π (i : ι), κ ilower_set α) :
(⨅ (i : ι) (j : κ i), f i j).compl = ⨆ (i : ι) (j : κ i), (f i j).compl

Principal sets #

def upper_set.Ici {α : Type u_1} [preorder α] (a : α) :

The smallest upper set containing a given element.

Equations
def upper_set.Ioi {α : Type u_1} [preorder α] (a : α) :

The smallest upper set containing a given element.

Equations
@[simp]
theorem upper_set.coe_Ici {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_set.coe_Ioi {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_set.mem_Ici_iff {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem upper_set.mem_Ioi_iff {α : Type u_1} [preorder α] {a b : α} :
theorem upper_set.Ioi_le_Ici {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_set.Ici_top {α : Type u_1} [preorder α] [order_bot α] :
@[simp]
theorem upper_set.Ioi_bot {α : Type u_1} [preorder α] [order_top α] :
@[simp]
theorem upper_set.Ici_sup {α : Type u_1} [semilattice_sup α] (a b : α) :
@[simp]
theorem upper_set.Ici_Sup {α : Type u_1} [complete_lattice α] (S : set α) :
upper_set.Ici (has_Sup.Sup S) = ⨅ (a : α) (H : a S), upper_set.Ici a
@[simp]
theorem upper_set.Ici_supr {α : Type u_1} {ι : Sort u_2} [complete_lattice α] (f : ι → α) :
upper_set.Ici (⨆ (i : ι), f i) = ⨅ (i : ι), upper_set.Ici (f i)
@[simp]
theorem upper_set.Ici_supr₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [complete_lattice α] (f : Π (i : ι), κ i → α) :
upper_set.Ici (⨆ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), upper_set.Ici (f i j)
def lower_set.Iic {α : Type u_1} [preorder α] (a : α) :

Principal lower set. set.Iic as a lower set. The smallest lower set containing a given element.

Equations
def lower_set.Iio {α : Type u_1} [preorder α] (a : α) :

Strict principal lower set. set.Iio as a lower set.

Equations
@[simp]
theorem lower_set.coe_Iic {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_set.coe_Iio {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_set.mem_Iic_iff {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem lower_set.mem_Iio_iff {α : Type u_1} [preorder α] {a b : α} :
theorem lower_set.Ioi_le_Ici {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_set.Iic_top {α : Type u_1} [preorder α] [order_top α] :
@[simp]
theorem lower_set.Iio_bot {α : Type u_1} [preorder α] [order_bot α] :
@[simp]
theorem lower_set.Iic_inf {α : Type u_1} [semilattice_inf α] (a b : α) :
@[simp]
@[simp]
theorem lower_set.Iic_Inf {α : Type u_1} [complete_lattice α] (S : set α) :
lower_set.Iic (has_Inf.Inf S) = ⨅ (a : α) (H : a S), lower_set.Iic a
@[simp]
theorem lower_set.Iic_infi {α : Type u_1} {ι : Sort u_2} [complete_lattice α] (f : ι → α) :
lower_set.Iic (⨅ (i : ι), f i) = ⨅ (i : ι), lower_set.Iic (f i)
@[simp]
theorem lower_set.Iic_infi₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [complete_lattice α] (f : Π (i : ι), κ i → α) :
lower_set.Iic (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), lower_set.Iic (f i j)
@[simp]