def Function.funEqOn {α : Type u} {β : Type v} (φ : α → Prop) (f g : α → β) : Prop

Equations

• Function.funEqOn φ f g = ∀ (a : α), φ a → f a = g a

theorem Function.funEqOn.of_subset {α : Type u} {β : Type v} {φ ψ : α → Prop} {f g : α → β} (e : funEqOn φ f g) (h : ∀ (a : α), ψ a → φ a) : funEqOn ψ f g