induced_inf — Mathlib

English

The topology induced by g distributes over finite infima: the induced of t1 ∧ t2 equals the infimum of the induced topologies.

Русский

Топология, индуцированная по g, распределяется по пересечению: индуцированная топология t1 ⊓ t2 равна пересечению индуцированных топологий.

LaTeX

$$$(t_1 \wedge t_2).induced g = t_1.induced g \wedge t_2.induced g$$$

Lean4

@[simp]
theorem induced_inf : (t₁ ⊓ t₂).induced g = t₁.induced g ⊓ t₂.induced g :=
  (gc_coinduced_induced g).u_inf

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