subset_union — Mathlib

English

Let G be a group and H, K, L be subgroups of G. Then H is contained in the union K ∪ L if and only if H ≤ K or H ≤ L.

Русский

Пусть G — группа, H, K, L — подгруппы. Тогда H ⊆ K ∪ L тогда эквивалентно H ≤ K или H ≤ L.

LaTeX

$$$$ (H : \\mathrm{Set} G) \\subseteq K \\cup L \\iff H \\le K \\lor H \\le L. $$$$

Lean4

@[to_additive]
theorem subset_union {H K L : S} : (H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L :=
  by
  refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (· xH) (· xH)⟩
  rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
  exact fun ⟨x, xH, xK⟩ y yH ↦
    (h <| mul_mem xH yH).elim ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
      (mul_mem_cancel_left <| (h xH).resolve_left xK).mp

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