α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
⊢ ∀ (s : Set β), s ∈ l₂ → (fun x => if p x then f x else g x) ⁻¹' s ∈ l₁
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂
h₁ : Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂
⊢ Tendsto (fun x => if p x then f x else g x) l₁ l₂
simp only [tendsto_def, mem_inf_principal] at *
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
⊢ (fun x => if p x then f x else g x) ⁻¹' s ∈ l₁
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
⊢ ∀ (s : Set β), s ∈ l₂ → (fun x => if p x then f x else g x) ⁻¹' s ∈ l₁
intro s hs
case h
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ x ∈ (fun x => if p x then f x else g x) ⁻¹' s
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
⊢ (fun x => if p x then f x else g x) ⁻¹' s ∈ l₁
filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
case h
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ (if p x then f x else g x) ∈ s
case h
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ x ∈ (fun x => if p x then f x else g x) ⁻¹' s
rw [mem_preimage]
case h.inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : p x
⊢ f x ∈ s

case h.inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : ¬p x
⊢ g x ∈ s
case h
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ (if p x then f x else g x) ∈ s
split_ifs with h
no goals
case h.inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : p x
⊢ f x ∈ s

case h.inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.319862
ι : Sort x
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ (s : Set β), s ∈ l₂ → {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : ¬p x
⊢ g x ∈ s
exacts [hp₀ h, hp₁ h]