gc_map_inl_toLeft — Mathlib

English

There is a Galois connection between map inl and toLeft: x ⊆ y^{toLeft} iff map_inl(x) ⊆ y.

Русский

Существует связь Галуа между отображением inl и проекцией на левую часть: x ⊆ y^{toLeft} эквивалентно map_inl(x) ⊆ y.

LaTeX

$$x \subseteq y^{\mathrm{toLeft}} \iff \mathrm{map} (\mathrm{inl}) \, x \subseteq y$$

Lean4

theorem gc_map_inl_toLeft : GaloisConnection (·.map (.inl : α ↪ α ⊕ β)) toLeft := fun _ _ ↦
  map_inl_subset_iff_subset_toLeft

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