α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
⊢ (⋃ (j : ι'), ⋂ (x : ↑I), eval ↑x ⁻¹' s (↑x) j) = ⋂ (x : ↑I), ⋃ (i : ι'), eval ↑x ⁻¹' s (↑x) i
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
⊢ (⋃ (j : ι'), pi I fun i => s i j) = pi I fun i => ⋃ (j : ι'), s i j
simp only [pi_def, biInter_eq_iInter, preimage_iUnion]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
this : Finite ↑I
⊢ (⋃ (j : ι'), ⋂ (x : ↑I), eval ↑x ⁻¹' s (↑x) j) = ⋂ (x : ↑I), ⋃ (i : ι'), eval ↑x ⁻¹' s (↑x) i
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
⊢ (⋃ (j : ι'), ⋂ (x : ↑I), eval ↑x ⁻¹' s (↑x) j) = ⋂ (x : ↑I), ⋃ (i : ι'), eval ↑x ⁻¹' s (↑x) i
haveI := hI.fintype.finite
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
this : Finite ↑I
i : ↑I
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval ↑i ⁻¹' s (↑i) j₁ ≤ eval ↑i ⁻¹' s (↑i) j₂
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
this : Finite ↑I
⊢ (⋃ (j : ι'), ⋂ (x : ↑I), eval ↑x ⁻¹' s (↑x) j) = ⋂ (x : ↑I), ⋃ (i : ι'), eval ↑x ⁻¹' s (↑x) i
refine' iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => _)
no goals
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
this : Finite ↑I
i : ↑I
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval ↑i ⁻¹' s (↑i) j₁ ≤ eval ↑i ⁻¹' s (↑i) j₂
exact preimage_mono <| hs i i.2 h