mulIndicator_rel_mulIndicator — Mathlib

English

If r is a relation with r(1,1) and ha: a ∈ s → r(f a, g a), then r(mulIndicator s f a, mulIndicator s g a) holds.

Русский

Если r — отношение, удовлетворяющее r(1,1) и ha: a ∈ s → r(f(a), g(a)), то выполняется r( mulIndicator s f a, mulIndicator s g a ).

LaTeX

$$r 1 1 → (a ∈ s → r (f a) (g a)) → r ((s.mulIndicator f) a) ((s.mulIndicator g) a)$$

Lean4

@[to_additive]
theorem mulIndicator_rel_mulIndicator {r : M → M → Prop} (h1 : r 1 1) (ha : a ∈ s → r (f a) (g a)) :
    r (mulIndicator s f a) (mulIndicator s g a) :=
  by
  simp only [mulIndicator]
  split_ifs with has
  exacts [ha has, h1]

Похожие утверждения