case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x

case neg
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
by_cases hx : x ∈ ⋃ i, s i
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ f x = ⨆ (i : ι), mulIndicator (s i) f x
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
rw [mulIndicator_of_mem hx]
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x = ⨆ (i : ι), mulIndicator (s i) f x
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ f x = ⨆ (i : ι), mulIndicator (s i) f x
rw [mem_iUnion] at hx
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x ≤ ⨆ (i : ι), mulIndicator (s i) f x
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x = ⨆ (i : ι), mulIndicator (s i) f x
refine' le_antisymm _ (iSup_le fun i => mulIndicator_le_self' (fun x _ => h1 ▸ bot_le) x)
case pos.intro
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ (i : ι), mulIndicator (s i) f x
case pos
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x ≤ ⨆ (i : ι), mulIndicator (s i) f x
rcases hx with ⟨i, hi⟩
no goals
case pos.intro
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ (i : ι), mulIndicator (s i) f x
exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)
case neg
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋃ (i : ι), s i
⊢ 1 = ⨆ (i : ι), mulIndicator (s i) f x
case neg
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
rw [mulIndicator_of_not_mem hx]
case neg
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (x_1 : ι), ¬x ∈ s x_1
⊢ 1 = ⨆ (i : ι), mulIndicator (s i) f x
case neg
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋃ (i : ι), s i
⊢ 1 = ⨆ (i : ι), mulIndicator (s i) f x
simp only [mem_iUnion, not_exists] at hx
no goals
case neg
α : Type u_3
β : Type ?u.157531
ι✝ : Type ?u.157534
M✝ : Type ?u.157537
N : Type ?u.157540
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_1
M : Type u_2
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (x_1 : ι), ¬x ∈ s x_1
⊢ 1 = ⨆ (i : ι), mulIndicator (s i) f x
simp [hx, ← h1]