inter — Mathlib

English

If two surjections onto t from s1 and s2 with an injectivity constraint on s1 ∪ s2 exist, then there is a surjection onto t from s1 ∩ s2.

Русский

Если существуют две сюръекции на t от s1 и s2 с инъективным ограничением на s1 ∪ s2, то существует сюръекция на t от s1 ∩ s2.

LaTeX

$$$\\text{SurjOn } f\\ s_1\\ t \\land \\text{SurjOn } f\\ s_2\\ t \\land \\text{InjOn } f\\ (s_1 \\cup s_2) \\Rightarrow \\text{SurjOn } f\\ (s_1 \\cap s_2)\\ t.$$$

Lean4

theorem inter (h₁ : SurjOn f s₁ t) (h₂ : SurjOn f s₂ t) (h : InjOn f (s₁ ∪ s₂)) : SurjOn f (s₁ ∩ s₂) t :=
  inter_self t ▸ h₁.inter_inter h₂ h

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