inter — Mathlib

English

The intersection of two blocks is a block.

Русский

Пересечение двух блоков является блоком.

LaTeX

$$$ \\text{IsBlock } G (B_1 \\cap B_2) $ given IsBlock G B1 and IsBlock G B2.$$

Lean4

/-- The intersection of two blocks is a block. -/
@[to_additive /-- The intersection of two blocks is a block. -/
    ]
theorem inter {B₁ B₂ : Set X} (h₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) : IsBlock G (B₁ ∩ B₂) :=
  by
  simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢
  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
  rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]

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