rcomap'_sets — Mathlib

English

The sets of rcomap' are precisely the image under SetRel of the relation {(s, t) | r.preimage s ⊆ t} applied to f.sets.

Русский

Множества rcomap' описываются как образ по отношению SetRel множества f.sets через отношение { (s, t) | r.preimage s ⊆ t }.

LaTeX

$$$ (\\mathrm{rcomap}'\\, r\\, f).\\mathrm{sets} = \\operatorname{SetRel.image}\\{(s,t) \\mid r.preimage s \\subseteq t\\} f.sets $$$

Lean4

theorem rcomap'_sets (r : SetRel α β) (f : Filter β) :
    (rcomap' r f).sets = SetRel.image {(s, t) | r.preimage s ⊆ t} f.sets :=
  rfl

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