mem_range_mulIndicator — Mathlib

English

The range of mulIndicator s f consists exactly of 1, when s ≠ univ, together with all values f takes on s.

Русский

Область значений mulIndicator s f состоит из 1 (если s ≠ univ) и всех значений f(x) для x ∈ s.

LaTeX

$$$r \\in range( mulIndicator\, s\, f) \\iff (r = 1 \\wedge s \\neq univ) \\lor r \\in f '' s$$$

Lean4

@[to_additive]
theorem mem_range_mulIndicator {r : M} {s : Set α} {f : α → M} :
    r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s := by
  simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm, @eq_comm _ r 1]

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