coinduced_sup — Mathlib

English

Coinduced distributes over supremum: coinduced f (t1 ⊔ t2) = coinduced f t1 ⊔ coinduced f t2.

Русский

Коиндуцированная по f топология распределена по верхнему пределу: коиндуцированная f (t1 ⊔ t2) = коиндуцированная f t1 ⊔ коиндуцированная f t2.

LaTeX

$$$\operatorname{coinduced} f (t_1 \sqcup t_2) = \operatorname{coinduced} f t_1 \sqcup \operatorname{coinduced} f t_2$$$

Lean4

@[simp]
theorem coinduced_sup : (t₁ ⊔ t₂).coinduced f = t₁.coinduced f ⊔ t₂.coinduced f :=
  (gc_coinduced_induced f).l_sup

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