Indicator #
Equations
- «term𝟭» = Lean.ParserDescr.node `«term𝟭» 1024 (Lean.ParserDescr.symbol "𝟭 ")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
indicate_apply
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[Semiring β]
{s : Finset α}
(x : α)
:
@[simp]
@[simp]
@[simp]
theorem
indicate_image
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[Semiring β]
{α' : Type u_5}
[DecidableEq α']
(e : α ≃ α')
(s : Finset α)
(a : α')
:
𝟭 (Finset.image (⇑e) s) a = 𝟭 s (e.symm a)
@[simp]
theorem
indicate_apply_eq_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[Semiring β]
{s : Finset α}
[Nontrivial β]
{a : α}
:
theorem
indicate_apply_ne_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[Semiring β]
{s : Finset α}
[Nontrivial β]
{a : α}
:
@[simp]
theorem
indicate_eq_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[Semiring β]
{s : Finset α}
[Nontrivial β]
:
theorem
indicate_ne_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[Semiring β]
{s : Finset α}
[Nontrivial β]
:
@[simp]
theorem
support_indicate
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[Semiring β]
{s : Finset α}
[Nontrivial β]
:
Function.support (𝟭 s) = ↑s
theorem
sum_indicate
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[Semiring β]
[Fintype α]
(s : Finset α)
:
theorem
indicate_inf_apply
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[CommSemiring β]
[Fintype α]
(s : Finset ι)
(t : ι → Finset α)
(x : α)
:
theorem
indicate_inf
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[CommSemiring β]
[Fintype α]
(s : Finset ι)
(t : ι → Finset α)
:
@[simp]
theorem
conj_indicate_apply
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[CommSemiring β]
[StarRing β]
(s : Finset α)
(a : α)
:
(starRingEnd β) (𝟭 s a) = 𝟭 s a
@[simp]
theorem
conj_indicate
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[CommSemiring β]
[StarRing β]
(s : Finset α)
:
(starRingEnd (α → β)) (𝟭 s) = 𝟭 s
@[simp]
theorem
indicate_nonneg
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[OrderedSemiring β]
{s : Finset α}
:
@[simp]
theorem
indicate_pos
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[OrderedSemiring β]
{s : Finset α}
[Nontrivial β]
:
theorem
Finset.Nonempty.indicate_pos
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[OrderedSemiring β]
{s : Finset α}
[Nontrivial β]
:
Alias of the reverse direction of indicate_pos
.
Normalised indicator #
Equations
- mu.termμ = Lean.ParserDescr.node `mu.termμ 1024 (Lean.ParserDescr.symbol "μ ")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
map_mu
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq α]
[DivisionSemiring β]
[DivisionSemiring γ]
(f : β →+* γ)
(s : Finset α)
(x : α)
:
theorem
mu_univ_eq_const
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[DivisionSemiring β]
[Fintype α]
:
mu Finset.univ = Function.const α (↑(Fintype.card α))⁻¹
@[simp]
theorem
mu_apply_eq_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[DivisionSemiring β]
{s : Finset α}
[CharZero β]
{a : α}
:
theorem
mu_apply_ne_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[DivisionSemiring β]
{s : Finset α}
[CharZero β]
{a : α}
:
@[simp]
theorem
mu_eq_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[DivisionSemiring β]
{s : Finset α}
[CharZero β]
:
theorem
mu_ne_zero
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[DivisionSemiring β]
{s : Finset α}
[CharZero β]
:
@[simp]
theorem
support_mu
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[DivisionSemiring β]
[CharZero β]
(s : Finset α)
:
Function.support (mu s) = ↑s
theorem
card_smul_mu
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[DivisionSemiring β]
[CharZero β]
(s : Finset α)
:
theorem
card_smul_mu_apply
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[DivisionSemiring β]
[CharZero β]
(s : Finset α)
(x : α)
:
@[simp]
theorem
conj_mu_apply
{α : Type u_2}
(β : Type u_3)
[DecidableEq α]
[Semifield β]
[StarRing β]
(s : Finset α)
(a : α)
:
(starRingEnd β) (mu s a) = mu s a
@[simp]
theorem
mu_nonneg
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[LinearOrderedSemifield β]
{s : Finset α}
:
@[simp]
theorem
mu_pos
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[LinearOrderedSemifield β]
{s : Finset α}
:
theorem
Finset.Nonempty.mu_pos
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[LinearOrderedSemifield β]
{s : Finset α}
:
Alias of the reverse direction of mu_pos
.