isBlockSystem — Mathlib

English

If B is a block and g ∈ G, then the translate g • B yields a block system by taking all translates {g • B | g ∈ G}.

Русский

Если B — блок, то все переносы g • B образуют систему блоков, образующую разбиение пространства.

LaTeX

$$$\\text{IsBlock}(G,B) \\Rightarrow \\text{BlockSystem}\\ G\\ (\\{g\\cdot B : g\\in G\\})$$$

Lean4

/-- Translates of a block form a block system -/
@[to_additive /-- Translates of a block form a block system -/
    ]
theorem isBlockSystem [hGX : MulAction.IsPretransitive G X] (hB : IsBlock G B) (hBe : B.Nonempty) :
    IsBlockSystem G (Set.range fun g : G => g • B) :=
  by
  refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
  case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g
  · simp only [Set.mem_range, not_exists]
    intro g hg
    apply hBe.ne_empty
    simpa only [Set.smul_set_eq_empty] using hg
  · intro a
    obtain ⟨b : X, hb : b ∈ B⟩ := hBe
    obtain ⟨g, rfl⟩ := exists_smul_eq G b a
    use g • B
    simp only [Set.smul_mem_smul_set_iff, hb, Set.mem_range, exists_apply_eq_apply, and_imp, forall_exists_index,
      forall_apply_eq_imp_iff, true_and]
    exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩

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