English
Let t1 be a topology on α and t2,t3 topologies on β. Then Continuous[t1, t2 ⊓ t3] f is equivalent to Continuous[t1,t2] f and Continuous[t1,t3] f.
Русский
Пусть t1 — топология на α, t2,t3 — топологии на β. Тогда Continuous[t1, t2 ⊓ t3] f эквивалентно Continuous[t1,t2] f и Continuous[t1,t3] f.
LaTeX
$$$$ \text{Continuous}[t_1, t_2 \wedge t_3] f \iff (\text{Continuous}[t_1,t_2] f \land \text{Continuous}[t_1,t_3] f). $$$$
Lean4
theorem continuous_inf_rng {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} :
Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f := by
simp only [continuous_iff_coinduced_le, le_inf_iff]
