map_comap_setCoe_val — Mathlib

English

For a subobject with coefficients from a set s, the map-comap relation reduces to principal: map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s.

Русский

Для подмножества s формула расщепляется на фиксацию через подмножество: map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s.

LaTeX

$$$ \\operatorname{map} (\\operatorname{Subtype.val}) ( \\operatorname{comap} (\\operatorname{Subtype.val}) f ) = f \\; \\inf \\; 𝓟\,s $$$

Lean4

theorem map_comap_setCoe_val (f : Filter β) (s : Set β) : (f.comap ((↑) : s → β)).map (↑) = f ⊓ 𝓟 s := by
  rw [map_comap, Subtype.range_val]

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