Supporting results for pointwise provable equality.

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

The fun Eq On construction in Function.

Equations

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

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